1 /-
2 Copyright (c) 2018 Kenny Lau. All rights reserved.
3 Released under Apache 2.0 license as described in the file LICENSE.
4 Authors: Kenny Lau
5
6 More operations on modules and ideals.
7 -/
8
9 import ring_theory.ideals data.nat.choose order.zorn
src └────────────────┘ └─────────────┘ └────────┘
10 import linear_algebra.tensor_product
src └───────────────────────────┘
11 import data.equiv.algebra
src └────────────────┘
12 import ring_theory.algebra_operations
src └────────────────────────────┘
13
14 universes u v w x
15
16 open lattice
17
18 namespace submodule
19
20 variables {R : Type u} {M : Type v}
21 variables [comm_ring R] [add_comm_group M] [module R M]
id └───────┘ └────────────┘ └────┘
src └───────┘ └────────────┘ └────┘
typ └───────┘ └────────────┘ └────┘
doc └────┘
22
23 instance has_scalar' : has_scalar (ideal R) (submodule R M) :=
id └────────┘ └───┘ ┴ └───────┘ ┴ ┴
src └────────┘ └───┘ └───────┘
typ └────────┘ └───┘ ┴ └───────┘ ┴ ┴
doc └────────┘ └───────┘
24 ⟨λ I N, ⨆ r : I, N.map (r.1 • linear_map.id)⟩
id ┴ ┴ ┴ ┴┴ ┴└──┘ ┴┴ ┴ └───────────┘
src ┴ ┴ └──┘ ┴ ┴ └───────────┘
typ ┴ ┴ ┴ ┴┴ ┴└──┘ ┴┴ ┴ └───────────┘
doc ┴ ┴ └──┘
25
26 def annihilator (N : submodule R M) : ideal R :=
27 (linear_map.lsmul R N).ker
28
29 def colon (N P : submodule R M) : ideal R :=
30 annihilator (P.map N.mkq)
31
32 variables {I J : ideal R} {N N₁ N₂ P P₁ P₂ : submodule R M}
33
34 theorem mem_annihilator {r} : r ∈ N.annihilator ↔ ∀ n ∈ N, r • n = (0:M) :=
35 ⟨λ hr n hn, congr_arg subtype.val (linear_map.ext_iff.1 (linear_map.mem_ker.1 hr) ⟨n, hn⟩),
36 λ h, linear_map.mem_ker.2 $ linear_map.ext $ λ n, subtype.eq $ h n.1 n.2⟩
37
38 theorem mem_annihilator' {r} : r ∈ N.annihilator ↔ N ≤ comap (r • linear_map.id) ⊥ :=
39 mem_annihilator.trans ⟨λ H n hn, (mem_bot R).2 $ H n hn, λ H n hn, (mem_bot R).1 $ H hn⟩
40
41 theorem annihilator_bot : (⊥ : submodule R M).annihilator = ⊤ :=
42 (ideal.eq_top_iff_one _).2 $ mem_annihilator'.2 bot_le
43
44 theorem annihilator_eq_top_iff : N.annihilator = ⊤ ↔ N = ⊥ :=
45 ⟨λ H, eq_bot_iff.2 $ λ (n:M) hn, (mem_bot R).2 $ one_smul R n ▸ mem_annihilator.1 ((ideal.eq_top_iff_one _).1 H) n hn,
46 λ H, H.symm ▸ annihilator_bot⟩
id └─────────────┘
src └─────────────┘
typ └─────────────┘
47
48 theorem annihilator_mono (h : N ≤ P) : P.annihilator ≤ N.annihilator :=
49 λ r hrp, mem_annihilator.2 $ λ n hn, mem_annihilator.1 hrp n $ h hn
50
51 theorem annihilator_supr (ι : Type w) (f : ι → submodule R M) :
52 (annihilator ⨆ i, f i) = ⨅ i, annihilator (f i) :=
53 le_antisymm (le_infi $ λ i, annihilator_mono $ le_supr _ _)
id └──────────────┘ └─────┘
src └──────────────┘ └─────┘
typ └──────────────┘ └─────┘
54 (λ r H, mem_annihilator'.2 $ supr_le $ λ i,
id └──────────────┘┴ └─────┘ ┴
src └──────────────┘┴ └─────┘
typ └──────────────┘┴ └─────┘ ┴
55 have _ := (mem_infi _).1 H i, mem_annihilator'.1 this)
id └──────┘ ┴ ┴ ┴ └──────────────┘┴ └──┘
src └──────┘ ┴ └──────────────┘┴
typ └──────┘ ┴ ┴ ┴ └──────────────┘┴ └──┘
56
57 theorem mem_colon {r} : r ∈ N.colon P ↔ ∀ p ∈ P, r • p ∈ N :=
id ┴ ┴ ┴└────┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴
src ┴ └────┘ ┴ ┴ ┴
typ ┴ ┴ ┴└────┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴
58 mem_annihilator.trans ⟨λ H p hp, (quotient.mk_eq_zero N).1 (H (quotient.mk p) (mem_map_of_mem hp)),
id └─────────────┘└────┘ ┴ ┴ └┘ └─────────────────┘ ┴ ┴ ┴ └─────────┘ ┴ └────────────┘ └┘
src └─────────────┘└────┘ └─────────────────┘ ┴ └─────────┘ └────────────┘
typ └─────────────┘└────┘ ┴ ┴ └┘ └─────────────────┘ ┴ ┴ ┴ └─────────┘ ┴ └────────────┘ └┘
doc └─────────┘
59 λ H m ⟨p, hp, hpm⟩, hpm ▸ (N.mkq).map_smul r p ▸ (quotient.mk_eq_zero N).2 $ H p hp⟩
id ┴ ┴ ┴┴ └┘ └─┘ ┴ ┴└──┘ └──────┘ ┴ ┴ └─────────────────┘ ┴ ┴ ┴
src ┴ └──┘ └──────┘ ┴ └─────────────────┘ ┴
typ ┴ ┴ ┴┴ └┘ └─┘ ┴ ┴└──┘ └──────┘ ┴ ┴ └─────────────────┘ ┴ ┴ ┴
doc └──┘
60
61 theorem mem_colon' {r} : r ∈ N.colon P ↔ P ≤ comap (r • linear_map.id) N :=
id ┴ ┴ ┴└────┘ ┴ ┴ ┴ ┴ └───┘ ┴ ┴ └───────────┘ ┴
src ┴ └────┘ ┴ ┴ └───┘ ┴ └───────────┘
typ ┴ ┴ ┴└────┘ ┴ ┴ ┴ ┴ └───┘ ┴ ┴ └───────────┘ ┴
doc └───┘
62 mem_colon
id └───────┘
src └───────┘
typ └───────┘
63
64 theorem colon_mono (hn : N₁ ≤ N₂) (hp : P₁ ≤ P₂) : N₁.colon P₂ ≤ N₂.colon P₁ :=
id └┘ ┴ └┘ └┘ ┴ └┘ └┘└────┘ └┘ ┴ └┘└────┘ └┘
src ┴ ┴ └────┘ ┴ └────┘
typ └┘ ┴ └┘ └┘ ┴ └┘ └┘└────┘ └┘ ┴ └┘└────┘ └┘
65 λ r hrnp, mem_colon.2 $ λ p₁ hp₁, hn $ mem_colon.1 hrnp p₁ $ hp hp₁
id ┴ └──┘ └───────┘┴ └┘ └─┘ └┘ └───────┘┴ └──┘ └┘ └┘ └─┘
src └───────┘┴ └───────┘┴
typ ┴ └──┘ └───────┘┴ └┘ └─┘ └┘ └───────┘┴ └──┘ └┘ └┘ └─┘
66
67 theorem infi_colon_supr (ι₁ : Type w) (f : ι₁ → submodule R M)
id └┘ └───────┘ ┴ ┴
src └───────┘
typ └┘ └───────┘ ┴ ┴
doc └───────┘
68 (ι₂ : Type x) (g : ι₂ → submodule R M) :
id └┘ └───────┘ ┴ ┴
src └───────┘
typ └┘ └───────┘ ┴ ┴
doc └───────┘
69 (⨅ i, f i).colon (⨆ j, g j) = ⨅ i j, (f i).colon (g j) :=
id ┴ ┴┴ ┴ ┴ └───┘ ┴ ┴┴ ┴ ┴ ┴ ┴ ┴ ┴┴ ┴ ┴ └───┘ ┴ ┴
src ┴ ┴ └───┘ ┴ ┴ ┴ ┴ ┴ └───┘
typ ┴ ┴┴ ┴ ┴ └───┘ ┴ ┴┴ ┴ ┴ ┴ ┴ ┴ ┴┴ ┴ ┴ └───┘ ┴ ┴
doc ┴ ┴ ┴ ┴ ┴ ┴
70 le_antisymm (le_infi $ λ i, le_infi $ λ j, colon_mono (infi_le _ _) (le_supr _ _))
id └─────────┘ └─────┘ ┴ └─────┘ ┴ └────────┘ └─────┘ └─────┘
src └─────────┘ └─────┘ └─────┘ └────────┘ └─────┘ └─────┘
typ └─────────┘ └─────┘ ┴ └─────┘ ┴ └────────┘ └─────┘ └─────┘
71 (λ r H, mem_colon'.2 $ supr_le $ λ j, map_le_iff_le_comap.1 $ le_infi $ λ i,
id ┴ ┴ └────────┘┴ └─────┘ ┴ └─────────────────┘┴ └─────┘ ┴
src └────────┘┴ └─────┘ └─────────────────┘┴ └─────┘
typ ┴ ┴ └────────┘┴ └─────┘ ┴ └─────────────────┘┴ └─────┘ ┴
72 map_le_iff_le_comap.2 $ mem_colon'.1 $ have _ := ((mem_infi _).1 H i),
id └─────────────────┘┴ └────────┘┴ └──────┘ ┴ ┴ ┴
src └─────────────────┘┴ └────────┘┴ └──────┘ ┴
typ └─────────────────┘┴ └────────┘┴ └──────┘ ┴ ┴ ┴
73 have _ := ((mem_infi _).1 this j), this)
id └──────┘ ┴ └──┘ ┴ └──┘
src └──────┘ ┴
typ └──────┘ ┴ └──┘ ┴ └──┘
74
75 theorem smul_mem_smul {r} {n} (hr : r ∈ I) (hn : n ∈ N) : r • n ∈ I • N :=
id ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴
src ┴ ┴ ┴ ┴ ┴
typ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴
76 (le_supr _ ⟨r, hr⟩ : _ ≤ I • N) ⟨n, hn, rfl⟩
id └─────┘ ┴ └┘ ┴ ┴ ┴ ┴ ┴ └┘ └─┘
src └─────┘ ┴ ┴ └─┘
typ └─────┘ ┴ └┘ ┴ ┴ ┴ ┴ ┴ └┘ └─┘
77
78 theorem smul_le {P : submodule R M} : I • N ≤ P ↔ ∀ (r ∈ I) (n ∈ N), r • n ∈ P :=
id └───────┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴
src └───────┘ ┴ ┴ ┴ ┴ ┴
typ └───────┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴
doc └───────┘
79 ⟨λ H r hr n hn, H $ smul_mem_smul hr hn,
id ┴ ┴ └┘ ┴ └┘ ┴ └───────────┘ └┘ └┘
src └───────────┘
typ ┴ ┴ └┘ ┴ └┘ ┴ └───────────┘ └┘ └┘
80 λ H, supr_le $ λ r, map_le_iff_le_comap.2 $ λ n hn, H r.1 r.2 n hn⟩
id ┴ └─────┘ ┴ └─────────────────┘┴ ┴ └┘ ┴ ┴┴ ┴┴ ┴ └┘
src └─────┘ └─────────────────┘┴ ┴ ┴
typ ┴ └─────┘ ┴ └─────────────────┘┴ ┴ └┘ ┴ ┴┴ ┴┴ ┴ └┘
81
82 @[elab_as_eliminator]
doc └────────────────┘
83 theorem smul_induction_on {p : M → Prop} {x} (H : x ∈ I • N)
id ┴ ┴ ┴ ┴ ┴ ┴
src ┴ ┴
typ ┴ ┴ ┴ ┴ ┴ ┴
84 (Hb : ∀ (r ∈ I) (n ∈ N), p (r • n)) (H0 : p 0)
id ┴┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴
src ┴
typ ┴┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴
85 (H1 : ∀ x y, p x → p y → p (x + y))
id ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴
src ┴
typ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴
86 (H2 : ∀ (c:R) n, p n → p (c • n)) : p x :=
id ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴
src ┴
typ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴
87 (@smul_le _ _ _ _ _ _ _ ⟨p, H0, H1, H2⟩).2 Hb H
id └─────┘ ┴ └┘ └┘ └┘ ┴ └┘ ┴
src └─────┘ ┴
typ └─────┘ ┴ └┘ └┘ └┘ ┴ └┘ ┴
88
89 theorem mem_smul_span_singleton {I : ideal R} {m : M} {x : M} :
id └───┘ ┴ ┴ ┴
src └───┘
typ └───┘ ┴ ┴ ┴
90 x ∈ I • span R ({m} : set M) ↔ ∃ y ∈ I, y • m = x :=
id ┴ ┴ ┴ ┴ └──┘ ┴ ┴┴ └─┘ ┴ ┴ ┴ ┴ ┴┴ ┴ ┴ ┴ ┴ ┴
src ┴ ┴ └──┘ ┴ └─┘ ┴ ┴ ┴ ┴ ┴
typ ┴ ┴ ┴ ┴ └──┘ ┴ ┴┴ └─┘ ┴ ┴ ┴ ┴ ┴┴ ┴ ┴ ┴ ┴ ┴
doc └──┘
91 ⟨λ hx, smul_induction_on hx
id └┘ └───────────────┘ └┘
src └───────────────┘
typ └┘ └───────────────┘ └┘
92 (λ r hri n hnm, let ⟨s, hs⟩ := mem_span_singleton.1 hnm in ⟨r * s, I.mul_mem_right hri, hs ▸ mul_smul r s m⟩)
id ┴ └─┘ ┴ └─┘ └─┘ ┴ └┘ └────────────────┘┴ └─┘ ┴ ┴ ┴└────────────┘ └─┘ ┴ └──────┘ ┴ ┴
src └────────────────┘┴ ┴ └────────────┘ ┴ └──────┘
typ ┴ └─┘ ┴ └─┘ └─┘ ┴ └┘ └────────────────┘┴ └─┘ ┴ ┴ ┴└────────────┘ └─┘ ┴ └──────┘ ┴ ┴
93 ⟨0, I.zero_mem, by rw [zero_smul]⟩
id ┴└───────┘ └───────┘
src └───────┘ └──┘└───────┘┴
typ ┴└───────┘ └──┘└───────┘┴
doc └──┘ ┴
txt └──┘ ┴
par └──┘ ┴
pid └┘ ┴
st └────────────┘┴
94 (λ m1 m2 ⟨y1, hyi1, hy1⟩ ⟨y2, hyi2, hy2⟩, ⟨y1 + y2, I.add_mem hyi1 hyi2, by rw [add_smul, hy1, hy2]⟩)
id └┘ └┘ ┴└┘ └──┘ ┴└┘ └──┘ ┴ ┴└──────┘ └──────┘ └─┘ └─┘
src ┴ └──────┘ └──┘└──────┘└┘ └┘ ┴
typ └┘ └┘ ┴└┘ └──┘ ┴└┘ └──┘ ┴ ┴└──────┘ └──┘└──────┘└┘└─┘└┘└─┘┴
doc └──┘ └┘ └┘ ┴
txt └──┘ └┘ └┘ ┴
par └──┘ └┘ └┘ ┴
pid └┘ └┘ └┘ ┴
st └───────────┘└───┘└───┘┴
95 (λ c r ⟨y, hyi, hy⟩, ⟨c * y, I.mul_mem_left hyi, by rw [mul_smul, hy]⟩),
id ┴ ┴ ┴┴ └─┘ ┴ ┴ ┴└───────────┘ └──────┘ └┘
src ┴ └───────────┘ └──┘└──────┘└┘ ┴
typ ┴ ┴ ┴┴ └─┘ ┴ ┴ ┴└───────────┘ └──┘└──────┘└┘└┘┴
doc └──┘ └┘ ┴
txt └──┘ └┘ ┴
par └──┘ └┘ ┴
pid └┘ └┘ ┴
st └───────────┘└──┘┴
96 λ ⟨y, hyi, hy⟩, hy ▸ smul_mem_smul hyi (subset_span $ set.mem_singleton m)⟩
id ┴ └─┘ └┘ ┴ └───────────┘ └─────────┘ └───────────────┘ ┴
src ┴ └───────────┘ └─────────┘ └───────────────┘
typ ┴ └─┘ └┘ ┴ └───────────┘ └─────────┘ └───────────────┘ ┴
97
98 theorem smul_le_right : I • N ≤ N :=
id ┴ ┴ ┴ ┴ ┴
src ┴ ┴
typ ┴ ┴ ┴ ┴ ┴
99 smul_le.2 $ λ r hr n, N.smul_mem r
id └─────┘┴ ┴ └┘ ┴ ┴└───────┘ ┴
src └─────┘┴ └───────┘
typ └─────┘┴ ┴ └┘ ┴ ┴└───────┘ ┴
100
101 theorem smul_mono (hij : I ≤ J) (hnp : N ≤ P) : I • N ≤ J • P :=
id ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴
src ┴ ┴ ┴ ┴ ┴
typ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴
102 smul_le.2 $ λ r hr n hn, smul_mem_smul (hij hr) (hnp hn)
id └─────┘┴ ┴ └┘ ┴ └┘ └───────────┘ └─┘ └┘ └─┘ └┘
src └─────┘┴ └───────────┘
typ └─────┘┴ ┴ └┘ ┴ └┘ └───────────┘ └─┘ └┘ └─┘ └┘
103
104 theorem smul_mono_left (h : I ≤ J) : I • N ≤ J • N :=
id ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴
src ┴ ┴ ┴ ┴
typ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴
105 smul_mono h (le_refl N)
id └───────┘ ┴ └─────┘ ┴
src └───────┘ └─────┘
typ └───────┘ ┴ └─────┘ ┴
106
107 theorem smul_mono_right (h : N ≤ P) : I • N ≤ I • P :=
id ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴
src ┴ ┴ ┴ ┴
typ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴
108 smul_mono (le_refl I) h
id └───────┘ └─────┘ ┴ ┴
src └───────┘ └─────┘
typ └───────┘ └─────┘ ┴ ┴
109
110 variables (I J N P)
111 @[simp] theorem smul_bot : I • (⊥ : submodule R M) = ⊥ :=
id ┴ ┴ ┴ └───────┘ ┴ ┴ ┴ ┴
src ┴ ┴ └───────┘ ┴ ┴
typ ┴ ┴ ┴ └───────┘ ┴ ┴ ┴ ┴
doc └──┘ └───────┘
112 eq_bot_iff.2 $ smul_le.2 $ λ r hri s hsb,
id └────────┘┴ └─────┘┴ ┴ └─┘ ┴ └─┘
src └────────┘┴ └─────┘┴
typ └────────┘┴ └─────┘┴ ┴ └─┘ ┴ └─┘
113 (submodule.mem_bot R).2 $ ((submodule.mem_bot R).1 hsb).symm ▸ smul_zero r
id └───────────────┘ ┴ ┴ └───────────────┘ ┴ ┴ └─┘ └──┘ ┴ └───────┘ ┴
src └───────────────┘ ┴ └───────────────┘ ┴ └──┘ ┴ └───────┘
typ └───────────────┘ ┴ ┴ └───────────────┘ ┴ ┴ └─┘ └──┘ ┴ └───────┘ ┴
114
115 @[simp] theorem bot_smul : (⊥ : ideal R) • N = ⊥ :=
id ┴ └───┘ ┴ ┴ ┴ ┴ ┴
src ┴ └───┘ ┴ ┴ ┴
typ ┴ └───┘ ┴ ┴ ┴ ┴ ┴
doc └──┘
116 eq_bot_iff.2 $ smul_le.2 $ λ r hrb s hsi,
id └────────┘┴ └─────┘┴ ┴ └─┘ ┴ └─┘
src └────────┘┴ └─────┘┴
typ └────────┘┴ └─────┘┴ ┴ └─┘ ┴ └─┘
117 (submodule.mem_bot R).2 $ ((submodule.mem_bot R).1 hrb).symm ▸ zero_smul _ s
id └───────────────┘ ┴ ┴ └───────────────┘ ┴ ┴ └─┘ └──┘ ┴ └───────┘ ┴
src └───────────────┘ ┴ └───────────────┘ ┴ └──┘ ┴ └───────┘
typ └───────────────┘ ┴ ┴ └───────────────┘ ┴ ┴ └─┘ └──┘ ┴ └───────┘ ┴
118
119 @[simp] theorem top_smul : (⊤ : ideal R) • N = N :=
id ┴ └───┘ ┴ ┴ ┴ ┴ ┴
src ┴ └───┘ ┴ ┴
typ ┴ └───┘ ┴ ┴ ┴ ┴ ┴
doc └──┘
120 le_antisymm smul_le_right $ λ r hri, one_smul R r ▸ smul_mem_smul mem_top hri
id └─────────┘ └───────────┘ ┴ └─┘ └──────┘ ┴ ┴ ┴ └───────────┘ └─────┘ └─┘
src └─────────┘ └───────────┘ └──────┘ ┴ └───────────┘ └─────┘
typ └─────────┘ └───────────┘ ┴ └─┘ └──────┘ ┴ ┴ ┴ └───────────┘ └─────┘ └─┘
121
122 theorem smul_sup : I • (N ⊔ P) = I • N ⊔ I • P :=
id ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴
src ┴ ┴ ┴ ┴ ┴ ┴
typ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴
123 le_antisymm (smul_le.2 $ λ r hri m hmnp, let ⟨n, hn, p, hp, hnpm⟩ := mem_sup.1 hmnp in
id └─────────┘ └─────┘┴ ┴ └─┘ ┴ └──┘ └─┘ └┘ └┘ └──┘ └─────┘┴ └──┘
src └─────────┘ └─────┘┴ └─────┘┴
typ └─────────┘ └─────┘┴ ┴ └─┘ ┴ └──┘ └─┘ └┘ └┘ └──┘ └─────┘┴ └──┘
124 mem_sup.2 ⟨_, smul_mem_smul hri hn, _, smul_mem_smul hri hp, hnpm ▸ (smul_add _ _ _).symm⟩)
id └─────┘┴ └───────────┘ └─┘ └───────────┘ └─┘ ┴ └──────┘ └──┘
src └─────┘┴ └───────────┘ └───────────┘ ┴ └──────┘ └──┘
typ └─────┘┴ └───────────┘ └─┘ └───────────┘ └─┘ ┴ └──────┘ └──┘
125 (sup_le (smul_mono_right le_sup_left)
id └────┘ └─────────────┘ └─────────┘
src └────┘ └─────────────┘ └─────────┘
typ └────┘ └─────────────┘ └─────────┘
126 (smul_mono_right le_sup_right))
id └─────────────┘ └──────────┘
src └─────────────┘ └──────────┘
typ └─────────────┘ └──────────┘
127
128 theorem sup_smul : (I ⊔ J) • N = I • N ⊔ J • N :=
id ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴
src ┴ ┴ ┴ ┴ ┴ ┴
typ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴
129 le_antisymm (smul_le.2 $ λ r hrij n hn, let ⟨ri, hri, rj, hrj, hrijr⟩ := mem_sup.1 hrij in
id └─────────┘ └─────┘┴ ┴ └──┘ ┴ └┘ └─┘ └─┘ └─┘ └───┘ └─────┘┴ └──┘
src └─────────┘ └─────┘┴ └─────┘┴
typ └─────────┘ └─────┘┴ ┴ └──┘ ┴ └┘ └─┘ └─┘ └─┘ └───┘ └─────┘┴ └──┘
130 mem_sup.2 ⟨_, smul_mem_smul hri hn, _, smul_mem_smul hrj hn, hrijr ▸ (add_smul _ _ _).symm⟩)
id └─────┘┴ └───────────┘ └┘ └───────────┘ └┘ ┴ └──────┘ └──┘
src └─────┘┴ └───────────┘ └───────────┘ ┴ └──────┘ └──┘
typ └─────┘┴ └───────────┘ └┘ └───────────┘ └┘ ┴ └──────┘ └──┘
131 (sup_le (smul_mono_left le_sup_left)
id └────┘ └────────────┘ └─────────┘
src └────┘ └────────────┘ └─────────┘
typ └────┘ └────────────┘ └─────────┘
132 (smul_mono_left le_sup_right))
id └────────────┘ └──────────┘
src └────────────┘ └──────────┘
typ └────────────┘ └──────────┘
133
134 theorem smul_assoc : (I • J) • N = I • (J • N) :=
id ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴
src ┴ ┴ ┴ ┴ ┴
typ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴
135 le_antisymm (smul_le.2 $ λ rs hrsij t htn,
id └─────────┘ └─────┘┴ └┘ └───┘ ┴ └─┘
src └─────────┘ └─────┘┴
typ └─────────┘ └─────┘┴ └┘ └───┘ ┴ └─┘
136 smul_induction_on hrsij
id └───────────────┘ └───┘
src └───────────────┘
typ └───────────────┘ └───┘
137 (λ r hr s hs, (@smul_eq_mul R _ r s).symm ▸ smul_smul r s t ▸ smul_mem_smul hr (smul_mem_smul hs htn))
id ┴ └┘ ┴ └┘ └─────────┘ ┴ ┴ ┴ └──┘ ┴ └───────┘ ┴ ┴ ┴ ┴ └───────────┘ └┘ └───────────┘ └┘ └─┘
src └─────────┘ └──┘ ┴ └───────┘ ┴ └───────────┘ └───────────┘
typ ┴ └┘ ┴ └┘ └─────────┘ ┴ ┴ ┴ └──┘ ┴ └───────┘ ┴ ┴ ┴ ┴ └───────────┘ └┘ └───────────┘ └┘ └─┘
138 ((zero_smul R t).symm ▸ submodule.zero_mem _)
id └───────┘ ┴ ┴ └──┘ ┴ └────────────────┘
src └───────┘ └──┘ ┴ └────────────────┘
typ └───────┘ ┴ ┴ └──┘ ┴ └────────────────┘
139 (λ x y, (add_smul x y t).symm ▸ submodule.add_mem _)
id ┴ ┴ └──────┘ ┴ ┴ ┴ └──┘ ┴ └───────────────┘
src └──────┘ └──┘ ┴ └───────────────┘
typ ┴ ┴ └──────┘ ┴ ┴ ┴ └──┘ ┴ └───────────────┘
140 (λ r s h, (@smul_eq_mul R _ r s).symm ▸ smul_smul r s t ▸ submodule.smul_mem _ _ h))
id ┴ ┴ ┴ └─────────┘ ┴ ┴ ┴ └──┘ ┴ └───────┘ ┴ ┴ ┴ ┴ └────────────────┘ ┴
src └─────────┘ └──┘ ┴ └───────┘ ┴ └────────────────┘
typ ┴ ┴ ┴ └─────────┘ ┴ ┴ ┴ └──┘ ┴ └───────┘ ┴ ┴ ┴ ┴ └────────────────┘ ┴
141 (smul_le.2 $ λ r hr sn hsn, suffices J • N ≤ submodule.comap (r • linear_map.id) ((I • J) • N), from this hsn,
id └─────┘┴ ┴ └┘ └┘ └─┘ ┴ ┴ ┴ ┴ └─────────────┘ ┴ ┴ └───────────┘ ┴ ┴ ┴ ┴ ┴ └──┘ └─┘
src └─────┘┴ ┴ ┴ └─────────────┘ ┴ └───────────┘ ┴ ┴
typ └─────┘┴ ┴ └┘ └┘ └─┘ ┴ ┴ ┴ ┴ └─────────────┘ ┴ ┴ └───────────┘ ┴ ┴ ┴ ┴ ┴ └──┘ └─┘
doc └─────────────┘
142 smul_le.2 $ λ s hs n hn, show r • (s • n) ∈ (I • J) • N, from mul_smul r s n ▸ smul_mem_smul (smul_mem_smul hr hs) hn)
id └─────┘┴ ┴ └┘ ┴ └┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ └──────┘ ┴ ┴ ┴ ┴ └───────────┘ └───────────┘ └┘ └┘ └┘
src └─────┘┴ ┴ ┴ ┴ ┴ ┴ └──────┘ ┴ └───────────┘ └───────────┘
typ └─────┘┴ ┴ └┘ ┴ └┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ └──────┘ ┴ ┴ ┴ ┴ └───────────┘ └───────────┘ └┘ └┘ └┘
143
144 variables (S : set R) (T : set M)
id └─┘ └─┘
src └─┘ └─┘
typ └─┘ └─┘
145
146 theorem span_smul_span : (ideal.span S) • (span R T) =
id └────────┘ ┴ ┴ └──┘ ┴ ┴ ┴
src └────────┘ ┴ └──┘ ┴
typ └────────┘ ┴ ┴ └──┘ ┴ ┴ ┴
doc └──┘
147 span R (⋃ (s ∈ S) (t ∈ T), {s • t}) :=
id └──┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴┴ ┴ ┴
src └──┘ ┴ ┴ ┴ ┴
typ └──┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴┴ ┴ ┴
doc └──┘ ┴ ┴
148 le_antisymm (smul_le.2 $ λ r hrS n hnT, span_induction hrS
id └─────────┘ └─────┘┴ ┴ └─┘ ┴ └─┘ └────────────┘ └─┘
src └─────────┘ └─────┘┴ └────────────┘
typ └─────────┘ └─────┘┴ ┴ └─┘ ┴ └─┘ └────────────┘ └─┘
doc └────────────┘
149 (λ r hrS, span_induction hnT
id ┴ └─┘ └────────────┘ └─┘
src └────────────┘
typ ┴ └─┘ └────────────┘ └─┘
doc └────────────┘
150 (λ n hnT, subset_span $ set.mem_bUnion hrS $
id ┴ └─┘ └─────────┘ └────────────┘ └─┘
src └─────────┘ └────────────┘
typ ┴ └─┘ └─────────┘ └────────────┘ └─┘
151 set.mem_bUnion hnT $ set.mem_singleton _)
id └────────────┘ └─┘ └───────────────┘
src └────────────┘ └───────────────┘
typ └────────────┘ └─┘ └───────────────┘
152 ((smul_zero r : r • 0 = (0:M)).symm ▸ submodule.zero_mem _)
id └───────┘ ┴ ┴ ┴ ┴ ┴ └──┘ ┴ └────────────────┘
src └───────┘ ┴ ┴ └──┘ ┴ └────────────────┘
typ └───────┘ ┴ ┴ ┴ ┴ ┴ └──┘ ┴ └────────────────┘
153 (λ x y, (smul_add r x y).symm ▸ submodule.add_mem _)
id ┴ ┴ └──────┘ ┴ ┴ ┴ └──┘ ┴ └───────────────┘
src └──────┘ └──┘ ┴ └───────────────┘
typ ┴ ┴ └──────┘ ┴ ┴ ┴ └──┘ ┴ └───────────────┘
154 (λ c m, by rw [smul_smul, mul_comm, mul_smul]; exact submodule.smul_mem _ _))
id ┴ ┴ └───────┘ └──────┘ └──────┘ └────────────────┘
src └──┘└───────┘└┘└──────┘└┘└──────┘┴ └────┘└────────────────┘└──┘
typ ┴ ┴ └──┘└───────┘└┘└──────┘└┘└──────┘┴ └────┘└────────────────┘└──┘
doc └──┘ └┘ └┘ ┴ └────┘ └──┘
txt └──┘ └┘ └┘ ┴ └────┘ └──┘
par └──┘ └┘ └┘ ┴ └────┘ └──┘
pid └┘ └┘ └┘ ┴ ┴ └──┘
st └────────────┘└────────┘└────────┘┴└────────────────────────────┘
155 ((zero_smul R n).symm ▸ submodule.zero_mem _)
id └───────┘ ┴ ┴ └──┘ ┴ └────────────────┘
src └───────┘ └──┘ ┴ └────────────────┘
typ └───────┘ ┴ ┴ └──┘ ┴ └────────────────┘
156 (λ r s, (add_smul r s n).symm ▸ submodule.add_mem _)
id ┴ ┴ └──────┘ ┴ ┴ ┴ └──┘ ┴ └───────────────┘
src └──────┘ └──┘ ┴ └───────────────┘
typ ┴ ┴ └──────┘ ┴ ┴ ┴ └──┘ ┴ └───────────────┘
157 (λ c r, by rw [smul_eq_mul, mul_smul]; exact submodule.smul_mem _ _)) $
id ┴ ┴ └─────────┘ └──────┘ └────────────────┘
src └──┘└─────────┘└┘└──────┘┴ └────┘└────────────────┘└──┘
typ ┴ ┴ └──┘└─────────┘└┘└──────┘┴ └────┘└────────────────┘└──┘
doc └──┘ └┘ ┴ └────┘ └──┘
txt └──┘ └┘ ┴ └────┘ └──┘
par └──┘ └┘ ┴ └────┘ └──┘
pid └┘ └┘ ┴ ┴ └──┘
st └──────────────┘└────────┘┴└────────────────────────────┘
158 span_le.2 $ set.bUnion_subset $ λ r hrS, set.bUnion_subset $ λ n hnT, set.singleton_subset_iff.2 $
id └─────┘┴ └───────────────┘ ┴ └─┘ └───────────────┘ ┴ └─┘ └──────────────────────┘┴
src └─────┘┴ └───────────────┘ └───────────────┘ └──────────────────────┘┴
typ └─────┘┴ └───────────────┘ ┴ └─┘ └───────────────┘ ┴ └─┘ └──────────────────────┘┴
159 smul_mem_smul (subset_span hrS) (subset_span hnT)
id └───────────┘ └─────────┘ └─┘ └─────────┘ └─┘
src └───────────┘ └─────────┘ └─────────┘
typ └───────────┘ └─────────┘ └─┘ └─────────┘ └─┘
160
161 end submodule
162
163 namespace ideal
164
165 section chinese_remainder
166 variables {R : Type u} [comm_ring R] {ι : Type v}
id ┴ └───────┘
src └───────┘
typ ┴ └───────┘
167
168 theorem exists_sub_one_mem_and_mem (s : finset ι) {f : ι → ideal R}
id └────┘ ┴ ┴ └───┘ ┴
src └────┘ └───┘
typ └────┘ ┴ ┴ └───┘ ┴
doc └────┘
169 (hf : ∀ i ∈ s, ∀ j ∈ s, i ≠ j → f i ⊔ f j = ⊤) (i : ι) (his : i ∈ s) :
id ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴
src ┴ ┴ ┴ ┴ ┴
typ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴
170 ∃ r : R, r - 1 ∈ f i ∧ ∀ j ∈ s, j ≠ i → r ∈ f j :=
id ┴ ┴┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴
src ┴ ┴ ┴ ┴ ┴ ┴ ┴
typ ┴ ┴┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴
171 begin
st └─────
172 have : ∀ j ∈ s, j ≠ i → ∃ r : R, ∃ H : r - 1 ∈ f i, r ∈ f j,
id ┴ ┴ ┴ ┴ ┴ ┴ ┴┴ ┴
src └─────┘ └───┘ ┴ ┴┴┴ ┴ ┴ └───┘ ┴┴└───┘ ┴┴└─┘ ┴ ┴ ┴┴ ┴ ┴ ┴
typ └─────┘ └───┘┴ ┴ ┴┴┴ ┴ ┴ └───┘┴ ┴┴└───┘ ┴┴└─┘┴┴ ┴┴┴┴ ┴ ┴┴┴
doc └─────┘ └───┘ ┴ ┴ ┴ ┴ ┴ └───┘ ┴ └───┘ ┴ └─┘ ┴ ┴ ┴ ┴ ┴ ┴
txt └─────┘ └───┘ ┴ ┴ ┴ ┴ ┴ └───┘ ┴ └───┘ ┴ └─┘ ┴ ┴ ┴ ┴ ┴ ┴
par └─────┘ └───┘ ┴ ┴ ┴ ┴ ┴ └───┘ ┴ └───┘ ┴ └─┘ ┴ ┴ ┴ ┴ ┴ ┴
pid └───┘└┘ └───┘ ┴ ┴ ┴ ┴ ┴ └───┘ ┴ └───┘ ┴ └─┘ ┴ ┴ ┴ ┴ ┴ ┴
st ────────────────────────────────────────────────────────────┘└─
173 { intros j hjs hji, specialize hf i his j hjs hji.symm,
id └┘ ┴ └─┘ ┴ └─┘ └──────┘
src └──────────────┘ └─────────┘ ┴ ┴ ┴ ┴ ┴└──────┘
typ └──────────────┘ └─────────┘└┘┴┴┴└─┘┴┴┴└─┘┴└──────┘
doc └──────────────┘ └─────────┘ ┴ ┴ ┴ ┴ ┴
txt └──────────────┘ └─────────┘ ┴ ┴ ┴ ┴ ┴
par └──────────────┘ └─────────┘ ┴ ┴ ┴ ┴ ┴
pid └────────┘ ┴ ┴ ┴ ┴ ┴ ┴
st ───┘└──────────────┘└──────────────────────────────────┘└─
174 rw [eq_top_iff_one, submodule.mem_sup] at hf,
id └────────────┘ └───────────────┘
src └──┘└────────────┘└┘└───────────────┘└─────┘
typ └──┘└────────────┘└┘└───────────────┘└─────┘
doc └──┘ └┘ └─────┘
txt └──┘ └┘ └─────┘
par └──┘ └┘ └─────┘
pid └┘ └┘ ┴└────┘
st ─────────────────────┘└─────────────────┘┴└────┘└─
175 rcases hf with ⟨r, hri, s, hsj, hrs⟩, refine ⟨1 - r, _, _⟩,
id └┘ ┴
src └─────┘ └─────────────────────────┘ └─────┘ └┘ ┴ └─────┘
typ └─────┘└┘└─────────────────────────┘ └─────┘ └┘ ┴┴└─────┘
doc └─────┘ └─────────────────────────┘ └─────┘ └┘ ┴ └─────┘
txt └─────┘ └─────────────────────────┘ └─────┘ └┘ ┴ └─────┘
par └─────┘ └─────────────────────────┘ └─────┘ └┘ ┴ └─────┘
pid ┴ └─────────────────────────┘ ┴ └┘ ┴ └─────┘
st ───────────────────────────────────────┘└────────────────────┘└─
176 { rw [sub_right_comm, sub_self, zero_sub], exact (f i).neg_mem hri },
id └────────────┘ └──────┘ └──────┘ ┴ ┴ └─┘
src └──┘└────────────┘└┘└──────┘└┘└──────┘┴ └────┘ ┴ └────────┘ ┴
typ └──┘└────────────┘└┘└──────┘└┘└──────┘┴ └────┘ ┴┴┴└────────┘└─┘┴
doc └──┘ └┘ └┘ ┴ └────┘ ┴ └────────┘ ┴
txt └──┘ └┘ └┘ ┴ └────┘ ┴ └────────┘ ┴
par └──┘ └┘ └┘ ┴ └────┘ ┴ └────────┘ ┴
pid └┘ └┘ └┘ ┴ ┴ ┴ └────────┘ ┴
st ─────┘└────────────────┘└────────┘└────────┘└─────────────────────────┘└┘└
177 { rw [← hrs, add_sub_cancel'], exact hsj } },
id └─┘ └─────────────┘ └─┘
src └────┘ └┘└─────────────┘┴ └────┘ ┴
typ └────┘└─┘└┘└─────────────┘┴ └────┘└─┘┴
doc └────┘ └┘ ┴ └────┘ ┴
txt └────┘ └┘ ┴ └────┘ ┴
par └────┘ └┘ ┴ └────┘ ┴
pid └──┘ └┘ ┴ ┴ ┴
st ──────────────┘└───────────────┘└───────────┘└──┘└
178 classical,
src └───────┘
typ └───────┘
doc └───────┘
txt └───────┘
par └───────┘
st ──────────┘└─
179 have : ∃ g : ι → R, (∀ j, g j - 1 ∈ f i) ∧ ∀ j ∈ s, j ≠ i → g j ∈ f j,
id ┴ ┴ ┴ ┴┴ ┴ ┴ ┴
src └─────┘┴└───┘ ┴ ┴ ┴┴ └┘ ┴ ┴ ┴ └─┘ ┴ ┴ └┘ ┴ └───┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴
typ └─────┘┴└───┘┴┴┴┴┴┴┴ └┘ ┴ ┴ ┴ └─┘ ┴ ┴ └┘ ┴ └───┘┴ ┴ ┴ ┴┴┴ ┴ ┴ ┴ ┴┴┴
doc └─────┘ └───┘ ┴ ┴ ┴ └┘ ┴ ┴ ┴ └─┘ ┴ ┴ └┘ ┴ └───┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴
txt └─────┘ └───┘ ┴ ┴ ┴ └┘ ┴ ┴ ┴ └─┘ ┴ ┴ └┘ ┴ └───┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴
par └─────┘ └───┘ ┴ ┴ ┴ └┘ ┴ ┴ ┴ └─┘ ┴ ┴ └┘ ┴ └───┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴
pid └───┘└┘ └───┘ ┴ ┴ ┴ └┘ ┴ ┴ ┴ └─┘ ┴ ┴ └┘ ┴ └───┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴
st ──────────────────────────────────────────────────────────────────────┘└─
180 { choose g hg1 hg2,
src └──────────────┘
typ └──────────────┘
doc └──────────────┘
txt └──────────────┘
par └──────────────┘
pid └┘└──────┘
st ───┘└──────────────┘└─
181 refine ⟨λ j, if H : j ∈ s ∧ j ≠ i then g j H.1 H.2 else 1, λ j, _, λ j, _⟩,
id └┘ ┴ ┴ ┴ ┴
src └─────┘ └──┘└┘└───┘ ┴ ┴ ┴ ┴ ┴ ┴ └────┘ ┴ ┴ └─┘ └─────────┘ └─────┘ └────┘
typ └─────┘ └──┘└┘└───┘ ┴ ┴┴┴┴┴ ┴ ┴┴└────┘┴┴ ┴ └─┘ └─────────┘ └─────┘ └────┘
doc └─────┘ └──┘ └───┘ ┴ ┴ ┴ ┴ ┴ ┴ └────┘ ┴ ┴ └─┘ └─────────┘ └─────┘ └────┘
txt └─────┘ └──┘ └───┘ ┴ ┴ ┴ ┴ ┴ ┴ └────┘ ┴ ┴ └─┘ └─────────┘ └─────┘ └────┘
par └─────┘ └──┘ └───┘ ┴ ┴ ┴ ┴ ┴ ┴ └────┘ ┴ ┴ └─┘ └─────────┘ └─────┘ └────┘
pid ┴ └──┘ └───┘ ┴ ┴ ┴ ┴ ┴ ┴ └────┘ ┴ ┴ └─┘ └─────────┘ └─────┘ └────┘
st ─────────────────────────────────────────────────────────────────────────────┘└─
182 { split_ifs with h, { apply hg1 }, rw sub_self, exact (f i).zero_mem },
id └──────┘ ┴ ┴
src └──────────────┘ └────┘ ┴ └─┘└──────┘ └────┘ ┴ └─────────┘
typ └──────────────┘ └────┘ ┴ └─┘└──────┘ └────┘ ┴┴┴└─────────┘
doc └──────────────┘ └────┘ ┴ └─┘ └────┘ ┴ └─────────┘
txt └──────────────┘ └────┘ ┴ └─┘ └────┘ ┴ └─────────┘
par └──────────────┘ └────┘ ┴ └─┘ └────┘ ┴ └─────────┘
pid ┴└────┘ ┴ ┴ ┴ ┴ ┴ └───────┘└┘
st ─────┘└──────────────┘└──┘└────────┘└┘└──────────┘└─────────────────────┘└┘└
183 { intros hjs hji, rw dif_pos, { apply hg2 }, exact ⟨hjs, hji⟩ } },
id └─────┘ └─┘ └─┘
src └────────────┘ └─┘└─────┘ └────┘ ┴ └────┘ └┘ └┘
typ └────────────┘ └─┘└─────┘ └────┘ ┴ └────┘ └─┘└┘└─┘└┘
doc └────────────┘ └─┘ └────┘ ┴ └────┘ └┘ └┘
txt └────────────┘ └─┘ └────┘ ┴ └────┘ └┘ └┘
par └────────────┘ └─┘ └────┘ ┴ └────┘ └┘ └┘
pid └──────┘ ┴ ┴ ┴ ┴ └┘ ┴┴
st ───────────────────┘└──────────┘└──┘└────────┘└┘└────────────────┘└──┘└
184 rcases this with ⟨g, hgi, hgj⟩, use (s.erase i).prod g, split,
id └──┘ └─────┘ ┴ ┴
src └─────┘ └─────────────────┘ └──┘ └─────┘┴ └─────┘ └───┘
typ └─────┘└──┘└─────────────────┘ └──┘ └─────┘┴┴└─────┘┴ └───┘
doc └─────┘ └─────────────────┘ └──┘ └─────┘┴ └─────┘ └───┘
txt └─────┘ └─────────────────┘ └──┘ ┴ └─────┘ └───┘
par └─────┘ └─────────────────┘ └──┘ ┴ └─────┘ └───┘
pid ┴ └─────────────────┘ ┴ ┴ └─────┘
st ───────────────────────────────┘└──────────────────────┘└─────┘└─
185 { rw [← quotient.eq, quotient.mk_one, ← finset.prod_hom _ (quotient.mk (f i))],
id └─────────┘ └─────────────┘ └─────────────┘ └─────────┘ ┴ ┴
src └────┘└─────────┘└┘└─────────────┘└──┘└─────────────┘└─┘ └─────────┘┴ ┴ └─┘
typ └────┘└─────────┘└┘└─────────────┘└──┘└─────────────┘└─┘ └─────────┘┴ ┴┴┴└─┘
doc └────┘ └┘ └──┘ └─┘ ┴ ┴ └─┘
txt └────┘ └┘ └──┘ └─┘ ┴ ┴ └─┘
par └────┘ └┘ └──┘ └─┘ ┴ ┴ └─┘
pid └──┘ └┘ └──┘ └─┘ ┴ ┴ └─┘
st ───┘└───────────────┘└───────────────┘└───────────────────────────────────────┘└──
186 apply finset.prod_eq_one, intros, rw [← quotient.mk_one, quotient.eq], apply hgi },
id └────────────────┘ └─────────────┘ └─────────┘
src └────┘└────────────────┘ └────┘ └────┘└─────────────┘└┘└─────────┘┴ └────┘ ┴
typ └────┘└────────────────┘ └────┘ └────┘└─────────────┘└┘└─────────┘┴ └────┘ ┴
doc └────┘ └────┘ └────┘ └┘ ┴ └────┘ ┴
txt └────┘ └────┘ └────┘ └┘ ┴ └────┘ ┴
par └────┘ └────┘ └────┘ └┘ ┴ └────┘ ┴
pid ┴ └──┘ └┘ ┴ ┴ ┴
st ───────────────────────────┘└──────┘└─────────────────────┘└───────────┘└───────────┘└┘└
187 intros j hjs hji, rw [← quotient.eq_zero_iff_mem, ← finset.prod_hom _ (quotient.mk (f j))],
id └──────────────────────┘ └─────────────┘ └─────────┘ ┴ ┴
src └──────────────┘ └────┘└──────────────────────┘└──┘└─────────────┘└─┘ └─────────┘┴ ┴ └─┘
typ └──────────────┘ └────┘└──────────────────────┘└──┘└─────────────┘└─┘ └─────────┘┴ ┴┴┴└─┘
doc └──────────────┘ └────┘ └──┘ └─┘ ┴ ┴ └─┘
txt └──────────────┘ └────┘ └──┘ └─┘ ┴ ┴ └─┘
par └──────────────┘ └────┘ └──┘ └─┘ ┴ ┴ └─┘
pid └────────┘ └──┘ └──┘ └─┘ ┴ ┴ └─┘
st ─────────────────┘└──────────────────────────────┘└───────────────────────────────────────┘└──
188 refine finset.prod_eq_zero (finset.mem_erase_of_ne_of_mem hji hjs) _,
id └─────────────────┘ └───────────────────────────┘ └─┘ └─┘
src └─────┘└─────────────────┘┴ └───────────────────────────┘┴ ┴ └─┘
typ └─────┘└─────────────────┘┴ └───────────────────────────┘┴└─┘┴└─┘└─┘
doc └─────┘ ┴ ┴ ┴ └─┘
txt └─────┘ ┴ ┴ ┴ └─┘
par └─────┘ ┴ ┴ ┴ └─┘
pid ┴ ┴ ┴ ┴ └─┘
st ─────────────────────────────────────────────────────────────────────┘└─
189 rw quotient.eq_zero_iff_mem, exact hgj j hjs hji
id └──────────────────────┘ └─┘ ┴ └─┘ └─┘
src └─┘└──────────────────────┘ └────┘ ┴ ┴ ┴ ┴
typ └─┘└──────────────────────┘ └────┘└─┘┴┴┴└─┘┴└─┘┴
doc └─┘ └────┘ ┴ ┴ ┴ ┴
txt └─┘ └────┘ ┴ ┴ ┴ ┴
par └─┘ └────┘ ┴ ┴ ┴ ┴
pid ┴ ┴ ┴ ┴ ┴ ┴
st ────────────────────────────┘└────────────────────┘
190 end
st └─┘
191
192 theorem exists_sub_mem [fintype ι] {f : ι → ideal R}
id └─────┘ ┴ ┴ └───┘ ┴
src └─────┘ └───┘
typ └─────┘ ┴ ┴ └───┘ ┴
doc └─────┘
193 (hf : ∀ i j, i ≠ j → f i ⊔ f j = ⊤) (g : ι → R) :
id ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴
src ┴ ┴ ┴ ┴
typ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴
194 ∃ r : R, ∀ i, r - g i ∈ f i :=
id ┴ ┴┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴
src ┴ ┴ ┴ ┴
typ ┴ ┴┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴
195 begin
st └─────
196 have : ∃ φ : ι → R, (∀ i, φ i - 1 ∈ f i) ∧ (∀ i j, i ≠ j → φ i ∈ f j),
id ┴ ┴ ┴ ┴┴ ┴ ┴ ┴ ┴
src └─────┘┴└───┘ ┴ ┴ ┴┴ └┘ ┴ ┴ ┴┴└─┘┴┴ ┴ └┘ ┴ └──┘ ┴ ┴┴┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴
typ └─────┘┴└───┘┴┴┴┴┴┴┴ └┘ ┴ ┴ ┴┴└─┘┴┴ ┴ └┘ ┴ └──┘ ┴ ┴┴┴ ┴ ┴ ┴ ┴ ┴┴┴ ┴
doc └─────┘ └───┘ ┴ ┴ ┴ └┘ ┴ ┴ ┴ └─┘ ┴ ┴ └┘ ┴ └──┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴
txt └─────┘ └───┘ ┴ ┴ ┴ └┘ ┴ ┴ ┴ └─┘ ┴ ┴ └┘ ┴ └──┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴
par └─────┘ └───┘ ┴ ┴ ┴ └┘ ┴ ┴ ┴ └─┘ ┴ ┴ └┘ ┴ └──┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴
pid └───┘└┘ └───┘ ┴ ┴ ┴ └┘ ┴ ┴ ┴ └─┘ ┴ ┴ └┘ ┴ └──┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴
st ──────────────────────────────────────────────────────────────────────┘└─
197 { have := exists_sub_one_mem_and_mem (finset.univ : finset ι) (λ i _ j _ hij, hf i j hij),
id └────────────────────────┘ └─────────┘ └────┘ ┴ └┘
src └──────┘└────────────────────────┘┴ └─────────┘└─┘└────┘┴ └┘ └────────────┘ ┴ ┴ ┴ ┴
typ └──────┘└────────────────────────┘┴ └─────────┘└─┘└────┘┴┴└┘ └────────────┘└┘┴ ┴ ┴ ┴
doc └──────┘ ┴ └─────────┘└─┘└────┘┴ └┘ └────────────┘ ┴ ┴ ┴ ┴
txt └──────┘ ┴ └─┘ ┴ └┘ └────────────┘ ┴ ┴ ┴ ┴
par └──────┘ ┴ └─┘ ┴ └┘ └────────────┘ ┴ ┴ ┴ ┴
pid └───┘└─┘ ┴ └─┘ ┴ └┘ └────────────┘ ┴ ┴ ┴ ┴
st ───┘└─────────────────────────────────────────────────────────────────────────────────────┘└─
198 choose φ hφ,
src └─────────┘
typ └─────────┘
doc └─────────┘
txt └─────────┘
par └─────────┘
pid └┘└─┘
st ──────────────┘└─
199 existsi λ i, φ i (finset.mem_univ i),
id ┴ └─────────────┘
src └──────┘ └──┘ ┴ ┴ └─────────────┘┴ ┴
typ └──────┘ └──┘┴┴ ┴ └─────────────┘┴ ┴
doc └──────┘ └──┘ ┴ ┴ ┴ ┴
txt └──────┘ └──┘ ┴ ┴ ┴ ┴
par └──────┘ └──┘ ┴ ┴ ┴ ┴
pid ┴ └──┘ ┴ ┴ ┴ ┴
st ───────────────────────────────────────┘└─
200 exact ⟨λ i, (hφ i _).1, λ i j hij, (hφ i _).2 j (finset.mem_univ j) hij.symm⟩ },
id └┘ └─────────────┘ └───┘
src └────┘ └──┘ ┴ └─────┘ └────────┘ ┴ └────┘ ┴ └─────────────┘┴ └┘ └───┘└┘
typ └────┘ └──┘ ┴ └─────┘ └────────┘ └┘┴ └────┘ ┴ └─────────────┘┴ └┘ └───┘└┘
doc └────┘ └──┘ ┴ └─────┘ └────────┘ ┴ └────┘ ┴ ┴ └┘ └┘
txt └────┘ └──┘ ┴ └─────┘ └────────┘ ┴ └────┘ ┴ ┴ └┘ └┘
par └────┘ └──┘ ┴ └─────┘ └────────┘ ┴ └────┘ ┴ ┴ └┘ └┘
pid ┴ └──┘ ┴ └─────┘ └────────┘ ┴ └────┘ ┴ ┴ └┘ ┴┴
st ─────────────────────────────────────────────────────────────────────────────────┘└┘└
201 rcases this with ⟨φ, hφ1, hφ2⟩,
id └──┘
src └─────┘ └─────────────────┘
typ └─────┘└──┘└─────────────────┘
doc └─────┘ └─────────────────┘
txt └─────┘ └─────────────────┘
par └─────┘ └─────────────────┘
pid ┴ └─────────────────┘
st ───────────────────────────────┘└─
202 use finset.univ.sum (λ i, g i * φ i),
id └─────────────┘ ┴ ┴ ┴
src └──┘└─────────────┘┴ └──┘ ┴ ┴┴┴ ┴ ┴
typ └──┘└─────────────┘┴ └──┘┴┴ ┴┴┴┴┴ ┴
doc └──┘└─────────────┘┴ └──┘ ┴ ┴ ┴ ┴ ┴
txt └──┘ ┴ └──┘ ┴ ┴ ┴ ┴ ┴
par └──┘ ┴ └──┘ ┴ ┴ ┴ ┴ ┴
pid ┴ ┴ └──┘ ┴ ┴ ┴ ┴ ┴
st ─────────────────────────────────────┘└─
203 intros i,
src └──────┘
typ └──────┘
doc └──────┘
txt └──────┘
par └──────┘
pid └┘
st ─────────┘└─
204 rw [← quotient.eq, ← finset.univ.sum_hom (quotient.mk (f i))],
id └─────────┘ └─────────────────┘ └─────────┘ ┴ ┴
src └────┘└─────────┘└──┘└─────────────────┘┴ └─────────┘┴ ┴ └─┘
typ └────┘└─────────┘└──┘└─────────────────┘┴ └─────────┘┴ ┴┴┴└─┘
doc └────┘ └──┘└─────────────────┘┴ ┴ ┴ └─┘
txt └────┘ └──┘ ┴ ┴ ┴ └─┘
par └────┘ └──┘ ┴ ┴ ┴ └─┘
pid └──┘ └──┘ ┴ ┴ ┴ └─┘
st ──────────────────┘└─────────────────────────────────────────┘└──
205 refine eq.trans (finset.sum_eq_single i _ _) _,
id └──────┘ └──────────────────┘ ┴
src └─────┘└──────┘┴ └──────────────────┘┴ └─────┘
typ └─────┘└──────┘┴ └──────────────────┘┴┴└─────┘
doc └─────┘ ┴ ┴ └─────┘
txt └─────┘ ┴ ┴ └─────┘
par └─────┘ ┴ ┴ └─────┘
pid ┴ ┴ ┴ └─────┘
st ───────────────────────────────────────────────┘└─
206 { intros j _ hji, rw quotient.eq_zero_iff_mem, exact (f i).mul_mem_left (hφ2 j i hji) },
id └──────────────────────┘ ┴ └─┘ ┴ ┴ └─┘
src └────────────┘ └─┘└──────────────────────┘ └────┘ ┴ └─────────────┘ ┴ ┴ ┴ └┘
typ └────────────┘ └─┘└──────────────────────┘ └────┘ ┴┴ └─────────────┘ └─┘┴┴┴┴┴└─┘└┘
doc └────────────┘ └─┘ └────┘ ┴ └─────────────┘ ┴ ┴ ┴ └┘
txt └────────────┘ └─┘ └────┘ ┴ └─────────────┘ ┴ ┴ ┴ └┘
par └────────────┘ └─┘ └────┘ ┴ └─────────────┘ ┴ ┴ ┴ └┘
pid └──────┘ ┴ ┴ ┴ └─────────────┘ ┴ ┴ ┴ ┴┴
st ───┘└────────────┘└───────────────────────────┘└───────────────────────────────────────┘└┘└
207 { intros hi, exact (hi $ finset.mem_univ i).elim },
id └┘ └─────────────┘ ┴
src └───────┘ └────┘ ┴ ┴└─────────────┘┴ └─────┘
typ └───────┘ └────┘ └┘┴ ┴└─────────────┘┴┴└─────┘
doc └───────┘ └────┘ ┴ ┴ ┴ └─────┘
txt └───────┘ └────┘ ┴ ┴ ┴ └─────┘
par └───────┘ └────┘ ┴ ┴ ┴ └─────┘
pid └─┘ ┴ ┴ ┴ ┴ └───┘└┘
st ───┘└───────┘└────────────────────────────────────┘└┘└
208 specialize hφ1 i, rw [← quotient.eq, quotient.mk_one] at hφ1,
id └─┘ ┴ └─────────┘ └─────────────┘
src └─────────┘ ┴ └────┘└─────────┘└┘└─────────────┘└──────┘
typ └─────────┘└─┘┴┴ └────┘└─────────┘└┘└─────────────┘└──────┘
doc └─────────┘ ┴ └────┘ └┘ └──────┘
txt └─────────┘ ┴ └────┘ └┘ └──────┘
par └─────────┘ ┴ └────┘ └┘ └──────┘
pid ┴ ┴ └──┘ └┘ ┴└─────┘
st ─────────────────┘└─────────────────┘└───────────────┘┴└─────┘└─
209 rw [quotient.mk_mul, hφ1, mul_one]
id └─────────────┘ └─┘ └─────┘
src └──┘└─────────────┘└┘ └┘└─────┘└┘
typ └──┘└─────────────┘└┘└─┘└┘└─────┘└┘
doc └──┘ └┘ └┘ └┘
txt └──┘ └┘ └┘ └┘
par └──┘ └┘ └┘ └┘
pid └┘ └┘ └┘ ┴┴
st ────────────────────┘└───┘└───────┘┴┴
210 end
st └─┘
211
212 def quotient_inf_to_pi_quotient (f : ι → ideal R) :
id ┴ └───┘ ┴
src └───┘
typ ┴ └───┘ ┴
213 (⨅ i, f i).quotient → Π i, (f i).quotient :=
id ┴ ┴┴ ┴ ┴ └──────┘ ┴ ┴ ┴ └──────┘
src ┴ ┴ └──────┘ └──────┘
typ ┴ ┴┴ ┴ ┴ └──────┘ ┴ ┴ ┴ └──────┘
doc ┴ ┴
214 @@quotient.lift _ _ (⨅ i, f i) (λ r i, ideal.quotient.mk (f i) r)
id └───────────┘ ┴ ┴┴ ┴ ┴ ┴ ┴ └───────────────┘ ┴ ┴ ┴
src └───────────┘ ┴ ┴ └───────────────┘
typ └───────────┘ ┴ ┴┴ ┴ ┴ ┴ ┴ └───────────────┘ ┴ ┴ ┴
doc ┴ ┴
215 (@pi.is_ring_hom_pi ι (λ i, (f i).quotient) _ R _ _ _)
id └───────────────┘ ┴ ┴ ┴ ┴ └──────┘ ┴
src └───────────────┘ └──────┘
typ └───────────────┘ ┴ ┴ ┴ ┴ └──────┘ ┴
216 (λ r hr, funext $ λ i, quotient.eq_zero_iff_mem.2 $ (submodule.mem_infi _).1 hr i)
id ┴ └┘ └────┘ ┴ └──────────────────────┘┴ └────────────────┘ ┴ └┘ ┴
src └────┘ └──────────────────────┘┴ └────────────────┘ ┴
typ ┴ └┘ └────┘ ┴ └──────────────────────┘┴ └────────────────┘ ┴ └┘ ┴
217
218 theorem is_ring_hom_quotient_inf_to_pi_quotient (f : ι → ideal R) :
id ┴ └───┘ ┴
src └───┘
typ ┴ └───┘ ┴
219 is_ring_hom (quotient_inf_to_pi_quotient f) :=
id └─────────┘ └─────────────────────────┘ ┴
src └─────────┘ └─────────────────────────┘
typ └─────────┘ └─────────────────────────┘ ┴
doc └─────────┘
220 @@quotient.is_ring_hom _ _ _
id └──────────────────┘
src └──────────────────┘
typ └──────────────────┘
221 (@pi.is_ring_hom_pi ι (λ i, (f i).quotient) _ R _ _ _) _
id └───────────────┘ ┴ ┴ ┴ ┴ └──────┘ ┴
src └───────────────┘ └──────┘
typ └───────────────┘ ┴ ┴ ┴ ┴ └──────┘ ┴
222
223 theorem bijective_quotient_inf_to_pi_quotient [fintype ι] {f : ι → ideal R}
id └─────┘ ┴ ┴ └───┘ ┴
src └─────┘ └───┘
typ └─────┘ ┴ ┴ └───┘ ┴
doc └─────┘
224 (hf : ∀ i j, i ≠ j → f i ⊔ f j = ⊤) :
id ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴
src ┴ ┴ ┴ ┴
typ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴
225 function.bijective (quotient_inf_to_pi_quotient f) :=
id └────────────────┘ └─────────────────────────┘ ┴
src └────────────────┘ └─────────────────────────┘
typ └────────────────┘ └─────────────────────────┘ ┴
226 ⟨λ x y, quotient.induction_on₂' x y $ λ r s hrs, quotient.eq.2 $
id ┴ ┴ └─────────────────────┘ ┴ ┴ ┴ ┴ └─┘ └─────────┘┴
src └─────────────────────┘ └─────────┘┴
typ ┴ ┴ └─────────────────────┘ ┴ ┴ ┴ ┴ └─┘ └─────────┘┴
227 (submodule.mem_infi _).2 $ λ i, quotient.eq.1 $
id └────────────────┘ ┴ ┴ └─────────┘┴
src └────────────────┘ ┴ └─────────┘┴
typ └────────────────┘ ┴ ┴ └─────────┘┴
228 show quotient_inf_to_pi_quotient f (quotient.mk' r) i = _, by rw hrs; refl,
id └─────────────────────────┘ ┴ └──────────┘ ┴ ┴ ┴ └─┘
src └─────────────────────────┘ └──────────┘ ┴ └─┘ └──┘
typ └─────────────────────────┘ ┴ └──────────┘ ┴ ┴ ┴ └─┘└─┘ └──┘
doc └─┘ └──┘
txt └─┘ └──┘
par └─┘ └──┘
pid ┴
st └───────────┘
229 λ g, let ⟨r, hr⟩ := exists_sub_mem hf (λ i, quotient.out' (g i)) in
id ┴ └─┘ ┴ └┘ └────────────┘ └┘ ┴ └───────────┘ ┴ ┴
src └────────────┘ └───────────┘
typ ┴ └─┘ ┴ └┘ └────────────┘ └┘ ┴ └───────────┘ ┴ ┴
230 ⟨quotient.mk _ r, funext $ λ i, quotient.out_eq' (g i) ▸ quotient.eq.2 (hr i)⟩⟩
id └─────────┘ └────┘ ┴ └──────────────┘ ┴ ┴ ┴ └─────────┘┴ ┴
src └─────────┘ └────┘ └──────────────┘ ┴ └─────────┘┴
typ └─────────┘ └────┘ ┴ └──────────────┘ ┴ ┴ ┴ └─────────┘┴ ┴
231
232 /-- Chinese Remainder Theorem. Eisenbud Ex.2.6. Similar to Atiyah-Macdonald 1.10 and Stacks 00DT -/
233 noncomputable def quotient_inf_ring_equiv_pi_quotient [fintype ι] (f : ι → ideal R)
id └─────┘ ┴ ┴ └───┘ ┴
src └─────┘ └───┘
typ └─────┘ ┴ ┴ └───┘ ┴
doc └─────┘
234 (hf : ∀ i j, i ≠ j → f i ⊔ f j = ⊤) :
id ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴
src ┴ ┴ ┴ ┴
typ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴
235 (⨅ i, f i).quotient ≃+* Π i, (f i).quotient :=
id ┴ ┴┴ ┴ ┴ └──────┘ └─┘ ┴ ┴ ┴ └──────┘
src ┴ ┴ └──────┘ └─┘ └──────┘
typ ┴ ┴┴ ┴ ┴ └──────┘ └─┘ ┴ ┴ ┴ └──────┘
doc ┴ ┴
236 by haveI : is_ring_hom (equiv.of_bijective (bijective_quotient_inf_to_pi_quotient hf)) :=
id └─────────┘ └────────────────┘ └───────────────────────────────────┘ └┘
src └──────┘└─────────┘┴ └────────────────┘┴ └───────────────────────────────────┘┴ └─────
typ └──────┘└─────────┘┴ └────────────────┘┴ └───────────────────────────────────┘┴└┘└─────
doc └──────┘└─────────┘┴ ┴ ┴ └─────
txt └──────┘ ┴ ┴ ┴ └─────
par └──────┘ ┴ ┴ ┴ └─────
pid ┴└┘ ┴ ┴ ┴ └┘└───
st └───────────────────────────────────────────────────────────────────────────────────────
237 is_ring_hom_quotient_inf_to_pi_quotient f;
id └─────────────────────────────────────┘ ┴
src ─┘└─────────────────────────────────────┘┴
typ ─┘└─────────────────────────────────────┘┴┴
doc ─┘ ┴
txt ─┘ ┴
par ─┘ ┴
pid ─┘ ┴
st ─────────────────────────────────────────────
238 exact ring_equiv.of (equiv.of_bijective (bijective_quotient_inf_to_pi_quotient hf))
id └───────────┘ └────────────────┘ └───────────────────────────────────┘ └┘
src └────┘└───────────┘┴ └────────────────┘┴ └───────────────────────────────────┘┴ └──
typ └────┘└───────────┘┴ └────────────────┘┴ └───────────────────────────────────┘┴└┘└──
doc └────┘└───────────┘┴ ┴ ┴ └──
txt └────┘ ┴ ┴ ┴ └──
par └────┘ ┴ ┴ ┴ └──
pid ┴ ┴ ┴ ┴ └┘└
st ────────────────────────────────────────────────────────────────────────────────────────
239
src ┘
typ ┘
doc ┘
txt ┘
par ┘
pid ┘
st ┘
240 end chinese_remainder
241
242 section mul_and_radical
243 variables {R : Type u} [comm_ring R]
id └───────┘
src └───────┘
typ └───────┘
244 variables {I J K L: ideal R}
id └───┘
src └───┘
typ └───┘
245
246 instance : has_mul (ideal R) := ⟨(•)⟩
id └─────┘ └───┘ ┴ ┴
src └─────┘ └───┘ ┴
typ └─────┘ └───┘ ┴ ┴
247
248 theorem mul_mem_mul {r s} (hr : r ∈ I) (hs : s ∈ J) : r * s ∈ I * J :=
id ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴
src ┴ ┴ ┴ ┴ ┴
typ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴
249 submodule.smul_mem_smul hr hs
id └─────────────────────┘ └┘ └┘
src └─────────────────────┘
typ └─────────────────────┘ └┘ └┘
250
251 theorem mul_mem_mul_rev {r s} (hr : r ∈ I) (hs : s ∈ J) : s * r ∈ I * J :=
id ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴
src ┴ ┴ ┴ ┴ ┴
typ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴
252 mul_comm r s ▸ mul_mem_mul hr hs
id └──────┘ ┴ ┴ ┴ └─────────┘ └┘ └┘
src └──────┘ ┴ └─────────┘
typ └──────┘ ┴ ┴ ┴ └─────────┘ └┘ └┘
253
254 theorem mul_le : I * J ≤ K ↔ ∀ (r ∈ I) (s ∈ J), r * s ∈ K :=
id ┴ ┴ ┴ ┴ ┴ ┴ ┴┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴
src ┴ ┴ ┴ ┴ ┴
typ ┴ ┴ ┴ ┴ ┴ ┴ ┴┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴
255 submodule.smul_le
id └───────────────┘
src └───────────────┘
typ └───────────────┘
256
257 variables (I J K)
258 protected theorem mul_comm : I * J = J * I :=
id ┴ ┴ ┴ ┴ ┴ ┴ ┴
src ┴ ┴ ┴
typ ┴ ┴ ┴ ┴ ┴ ┴ ┴
259 le_antisymm (mul_le.2 $ λ r hrI s hsJ, mul_mem_mul_rev hsJ hrI)
id └─────────┘ └────┘┴ ┴ └─┘ ┴ └─┘ └─────────────┘ └─┘ └─┘
src └─────────┘ └────┘┴ └─────────────┘
typ └─────────┘ └────┘┴ ┴ └─┘ ┴ └─┘ └─────────────┘ └─┘ └─┘
260 (mul_le.2 $ λ r hrJ s hsI, mul_mem_mul_rev hsI hrJ)
id └────┘┴ ┴ └─┘ ┴ └─┘ └─────────────┘ └─┘ └─┘
src └────┘┴ └─────────────┘
typ └────┘┴ ┴ └─┘ ┴ └─┘ └─────────────┘ └─┘ └─┘
261
262 protected theorem mul_assoc : (I * J) * K = I * (J * K) :=
id ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴
src ┴ ┴ ┴ ┴ ┴
typ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴
263 submodule.smul_assoc I J K
id └──────────────────┘ ┴ ┴ ┴
src └──────────────────┘
typ └──────────────────┘ ┴ ┴ ┴
264
265 theorem span_mul_span (S T : set R) : span S * span T =
id └─┘ ┴ └──┘ ┴ ┴ └──┘ ┴ ┴
src └─┘ └──┘ ┴ └──┘ ┴
typ └─┘ ┴ └──┘ ┴ ┴ └──┘ ┴ ┴
266 span ⋃ (s ∈ S) (t ∈ T), {s * t} :=
id └──┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴┴ ┴ ┴
src └──┘ ┴ ┴ ┴ ┴
typ └──┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴┴ ┴ ┴
doc ┴ ┴
267 submodule.span_smul_span S T
id └──────────────────────┘ ┴ ┴
src └──────────────────────┘
typ └──────────────────────┘ ┴ ┴
268 variables {I J K}
269
270 theorem mul_le_inf : I * J ≤ I ⊓ J :=
id ┴ ┴ ┴ ┴ ┴ ┴ ┴
src ┴ ┴ ┴
typ ┴ ┴ ┴ ┴ ┴ ┴ ┴
271 mul_le.2 $ λ r hri s hsj, ⟨I.mul_mem_right hri, J.mul_mem_left hsj⟩
id └────┘┴ ┴ └─┘ ┴ └─┘ ┴└────────────┘ └─┘ ┴└───────────┘ └─┘
src └────┘┴ └────────────┘ └───────────┘
typ └────┘┴ ┴ └─┘ ┴ └─┘ ┴└────────────┘ └─┘ ┴└───────────┘ └─┘
272
273 theorem mul_eq_inf_of_coprime (h : I ⊔ J = ⊤) : I * J = I ⊓ J :=
id ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴
src ┴ ┴ ┴ ┴ ┴ ┴
typ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴
274 le_antisymm mul_le_inf $ λ r ⟨hri, hrj⟩,
id └─────────┘ └────────┘ ┴ ┴└─┘ └─┘
src └─────────┘ └────────┘
typ └─────────┘ └────────┘ ┴ ┴└─┘ └─┘
275 let ⟨s, hsi, t, htj, hst⟩ := submodule.mem_sup.1 ((eq_top_iff_one _).1 h) in
id └─┘ ┴ └─┘ ┴ └─┘ └─┘ └───────────────┘┴ └────────────┘ ┴ ┴
src └───────────────┘┴ └────────────┘ ┴
typ └─┘ ┴ └─┘ ┴ └─┘ └─┘ └───────────────┘┴ └────────────┘ ┴ ┴
276 mul_one r ▸ hst ▸ (mul_add r s t).symm ▸ ideal.add_mem (I * J) (mul_mem_mul_rev hsi hrj) (mul_mem_mul hri htj)
id └─────┘ ┴ ┴ ┴ └─────┘ ┴ └──┘ ┴ └───────────┘ ┴ ┴ ┴ └─────────────┘ └─────────┘
src └─────┘ ┴ ┴ └─────┘ └──┘ ┴ └───────────┘ ┴ └─────────────┘ └─────────┘
typ └─────┘ ┴ ┴ ┴ └─────┘ ┴ └──┘ ┴ └───────────┘ ┴ ┴ ┴ └─────────────┘ └─────────┘
277
278 variables (I)
279 theorem mul_bot : I * ⊥ = ⊥ :=
id ┴ ┴ ┴ ┴ ┴
src ┴ ┴ ┴ ┴
typ ┴ ┴ ┴ ┴ ┴
280 submodule.smul_bot I
id └────────────────┘ ┴
src └────────────────┘
typ └────────────────┘ ┴
281
282 theorem bot_mul : ⊥ * I = ⊥ :=
id ┴ ┴ ┴ ┴ ┴
src ┴ ┴ ┴ ┴
typ ┴ ┴ ┴ ┴ ┴
283 submodule.bot_smul I
id └────────────────┘ ┴
src └────────────────┘
typ └────────────────┘ ┴
284
285 theorem mul_top : I * ⊤ = I :=
id ┴ ┴ ┴ ┴ ┴
src ┴ ┴ ┴
typ ┴ ┴ ┴ ┴ ┴
286 ideal.mul_comm ⊤ I ▸ submodule.top_smul I
id └────────────┘ ┴ ┴ ┴ └────────────────┘ ┴
src └────────────┘ ┴ ┴ └────────────────┘
typ └────────────┘ ┴ ┴ ┴ └────────────────┘ ┴
287
288 theorem top_mul : ⊤ * I = I :=
id ┴ ┴ ┴ ┴ ┴
src ┴ ┴ ┴
typ ┴ ┴ ┴ ┴ ┴
289 submodule.top_smul I
id └────────────────┘ ┴
src └────────────────┘
typ └────────────────┘ ┴
290 variables {I}
291
292 theorem mul_mono (hik : I ≤ K) (hjl : J ≤ L) : I * J ≤ K * L :=
id ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴
src ┴ ┴ ┴ ┴ ┴
typ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴
293 submodule.smul_mono hik hjl
id └─────────────────┘ └─┘ └─┘
src └─────────────────┘
typ └─────────────────┘ └─┘ └─┘
294
295 theorem mul_mono_left (h : I ≤ J) : I * K ≤ J * K :=
id ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴
src ┴ ┴ ┴ ┴
typ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴
296 submodule.smul_mono_left h
id └──────────────────────┘ ┴
src └──────────────────────┘
typ └──────────────────────┘ ┴
297
298 theorem mul_mono_right (h : J ≤ K) : I * J ≤ I * K :=
id ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴
src ┴ ┴ ┴ ┴
typ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴
299 submodule.smul_mono_right h
id └───────────────────────┘ ┴
src └───────────────────────┘
typ └───────────────────────┘ ┴
300
301 variables (I J K)
302 theorem mul_sup : I * (J ⊔ K) = I * J ⊔ I * K :=
id ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴
src ┴ ┴ ┴ ┴ ┴ ┴
typ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴
303 submodule.smul_sup I J K
id └────────────────┘ ┴ ┴ ┴
src └────────────────┘
typ └────────────────┘ ┴ ┴ ┴
304
305 theorem sup_mul : (I ⊔ J) * K = I * K ⊔ J * K :=
id ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴
src ┴ ┴ ┴ ┴ ┴ ┴
typ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴
306 submodule.sup_smul I J K
id └────────────────┘ ┴ ┴ ┴
src └────────────────┘
typ └────────────────┘ ┴ ┴ ┴
307 variables {I J K}
308
309 lemma pow_le_pow {m n : ℕ} (h : m ≤ n) :
id ┴ ┴ ┴ ┴
src ┴ ┴
typ ┴ ┴ ┴ ┴
310 I^n ≤ I^m :=
id ┴┴┴ ┴ ┴┴┴
src ┴ ┴ ┴
typ ┴┴┴ ┴ ┴┴┴
311 begin
st └─────
312 cases nat.exists_eq_add_of_le h with k hk,
id └─────────────────────┘ ┴
src └────┘└─────────────────────┘┴ └────────┘
typ └────┘└─────────────────────┘┴┴└────────┘
doc └────┘ ┴ └────────┘
txt └────┘ ┴ └────────┘
par └────┘ ┴ └────────┘
pid ┴ ┴ └────────┘
st ──────────────────────────────────────────┘└─
313 rw [hk, pow_add],
id └┘ └─────┘
src └──┘ └┘└─────┘┴
typ └──┘└┘└┘└─────┘┴
doc └──┘ └┘ ┴
txt └──┘ └┘ ┴
par └──┘ └┘ ┴
pid └┘ └┘ ┴
st ───────┘└───────┘└──
314 exact le_trans (mul_le_inf) (lattice.inf_le_left)
id └──────┘ └────────┘ └─────────────────┘
src └────┘└──────┘┴ └────────┘└┘ └─────────────────┘└┘
typ └────┘└──────┘┴ └────────┘└┘ └─────────────────┘└┘
doc └────┘ ┴ └┘ └┘
txt └────┘ ┴ └┘ └┘
par └────┘ ┴ └┘ └┘
pid ┴ ┴ └┘ ┴┴
st ───────────────────────────────────────────────────┘
315 end
st └─┘
316
317 /-- The radical of an ideal `I` consists of the elements `r` such that `r^n ∈ I` for some `n`. -/
318 def radical (I : ideal R) : ideal R :=
id └───┘ ┴ └───┘ ┴
src └───┘ └───┘
typ └───┘ ┴ └───┘ ┴
319 { carrier := { r | ∃ n : ℕ, r ^ n ∈ I },
id ┴ ┴ ┴ ┴┴ ┴ ┴ ┴ ┴ ┴
src ┴ ┴ ┴┴ ┴ ┴
typ ┴ ┴ ┴ ┴┴ ┴ ┴ ┴ ┴ ┴
320 zero := ⟨1, (pow_one (0:R)).symm ▸ I.zero_mem⟩,
id └─────┘ ┴ └──┘ ┴ ┴└───────┘
src └─────┘ └──┘ ┴ └───────┘
typ └─────┘ ┴ └──┘ ┴ ┴└───────┘
321 add := λ x y ⟨m, hxmi⟩ ⟨n, hyni⟩, ⟨m + n,
id ┴ ┴ ┴┴ └──┘ ┴┴ └──┘ ┴
src ┴
typ ┴ ┴ ┴┴ └──┘ ┴┴ └──┘ ┴
322 (add_pow x y (m + n)).symm ▸ I.sum_mem $
id └─────┘ ┴ ┴ ┴ └──┘ ┴ ┴└──────┘
src └─────┘ ┴ └──┘ ┴ └──────┘
typ └─────┘ ┴ ┴ ┴ └──┘ ┴ ┴└──────┘
doc └─────┘
323 show ∀ c ∈ finset.range (nat.succ (m + n)), x ^ c * y ^ (m + n - c) * (nat.choose (m + n) c) ∈ I,
id ┴ └──────────┘ └──────┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ └────────┘ ┴ ┴ ┴ ┴
src └──────────┘ └──────┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ └────────┘ ┴ ┴
typ ┴ └──────────┘ └──────┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ └────────┘ ┴ ┴ ┴ ┴
doc └──────────┘ └────────┘
324 from λ c hc, or.cases_on (le_total c m)
id ┴ └┘ └─────────┘ └──────┘ ┴
src └─────────┘ └──────┘
typ ┴ └┘ └─────────┘ └──────┘ ┴
325 (λ hcm, I.mul_mem_right $ I.mul_mem_left $ nat.add_comm n m ▸ (nat.add_sub_assoc hcm n).symm ▸
id └─┘ ┴└────────────┘ ┴└───────────┘ └──────────┘ ┴ └───────────────┘ └─┘ └──┘ ┴
src └────────────┘ └───────────┘ └──────────┘ ┴ └───────────────┘ └──┘ ┴
typ └─┘ ┴└────────────┘ ┴└───────────┘ └──────────┘ ┴ └───────────────┘ └─┘ └──┘ ┴
326 (pow_add y n (m-c)).symm ▸ I.mul_mem_right hyni)
id └─────┘ ┴ ┴┴ └──┘ ┴ ┴└────────────┘
src └─────┘ ┴ └──┘ ┴ └────────────┘
typ └─────┘ ┴ ┴┴ └──┘ ┴ ┴└────────────┘
327 (λ hmc, I.mul_mem_right $ I.mul_mem_right $ nat.add_sub_cancel' hmc ▸
id └─┘ ┴└────────────┘ ┴└────────────┘ └─────────────────┘ └─┘ ┴
src └────────────┘ └────────────┘ └─────────────────┘ ┴
typ └─┘ ┴└────────────┘ ┴└────────────┘ └─────────────────┘ └─┘ ┴
328 (pow_add x m (c-m)).symm ▸ I.mul_mem_right hxmi)⟩,
id └─────┘ ┴ ┴┴ └──┘ ┴ ┴└────────────┘
src └─────┘ ┴ └──┘ ┴ └────────────┘
typ └─────┘ ┴ ┴┴ └──┘ ┴ ┴└────────────┘
329 smul := λ r s ⟨n, hsni⟩, ⟨n, show (r * s)^n ∈ I,
id ┴ ┴ ┴┴ └──┘ ┴ ┴ ┴ ┴ ┴ ┴
src ┴ ┴ ┴
typ ┴ ┴ ┴┴ └──┘ ┴ ┴ ┴ ┴ ┴ ┴
330 from (mul_pow r s n).symm ▸ I.mul_mem_left hsni⟩ }
id └─────┘ ┴ ┴ └──┘ ┴ ┴└───────────┘
src └─────┘ └──┘ ┴ └───────────┘
typ └─────┘ ┴ ┴ └──┘ ┴ ┴└───────────┘
331
332 theorem le_radical : I ≤ radical I :=
id ┴ ┴ └─────┘ ┴
src ┴ └─────┘
typ ┴ ┴ └─────┘ ┴
doc └─────┘
333 λ r hri, ⟨1, (pow_one r).symm ▸ hri⟩
id ┴ └─┘ └─────┘ ┴ └──┘ ┴ └─┘
src └─────┘ └──┘ ┴
typ ┴ └─┘ └─────┘ ┴ └──┘ ┴ └─┘
334
335 variables (R)
336 theorem radical_top : (radical ⊤ : ideal R) = ⊤ :=
id └─────┘ ┴ └───┘ ┴ ┴ ┴
src └─────┘ ┴ └───┘ ┴ ┴
typ └─────┘ ┴ └───┘ ┴ ┴ ┴
doc └─────┘
337 (eq_top_iff_one _).2 ⟨0, submodule.mem_top⟩
id └────────────┘ ┴ └───────────────┘
src └────────────┘ ┴ └───────────────┘
typ └────────────┘ ┴ └───────────────┘
338 variables {R}
339
340 theorem radical_mono (H : I ≤ J) : radical I ≤ radical J :=
id ┴ ┴ ┴ └─────┘ ┴ ┴ └─────┘ ┴
src ┴ └─────┘ ┴ └─────┘
typ ┴ ┴ ┴ └─────┘ ┴ ┴ └─────┘ ┴
doc └─────┘ └─────┘
341 λ r ⟨n, hrni⟩, ⟨n, H hrni⟩
id ┴ ┴┴ └──┘ ┴
typ ┴ ┴┴ └──┘ ┴
342
343 variables (I)
344 theorem radical_idem : radical (radical I) = radical I :=
id └─────┘ └─────┘ ┴ ┴ └─────┘ ┴
src └─────┘ └─────┘ ┴ └─────┘
typ └─────┘ └─────┘ ┴ ┴ └─────┘ ┴
doc └─────┘ └─────┘ └─────┘
345 le_antisymm (λ r ⟨n, k, hrnki⟩, ⟨n * k, (pow_mul r n k).symm ▸ hrnki⟩) le_radical
id └─────────┘ ┴ ┴┴ ┴ └───┘ ┴ └─────┘ ┴ └──┘ ┴ └────────┘
src └─────────┘ ┴ └─────┘ └──┘ ┴ └────────┘
typ └─────────┘ ┴ ┴┴ ┴ └───┘ ┴ └─────┘ ┴ └──┘ ┴ └────────┘
346 variables {I}
347
348 theorem radical_eq_top : radical I = ⊤ ↔ I = ⊤ :=
id └─────┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴
src └─────┘ ┴ ┴ ┴ ┴ ┴
typ └─────┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴
doc └─────┘
349 ⟨λ h, (eq_top_iff_one _).2 $ let ⟨n, hn⟩ := (eq_top_iff_one _).1 h in
id ┴ └────────────┘ ┴ └─┘ ┴ └┘ └────────────┘ ┴ ┴
src └────────────┘ ┴ └────────────┘ ┴
typ ┴ └────────────┘ ┴ └─┘ ┴ └┘ └────────────┘ ┴ ┴
350 @one_pow R _ n ▸ hn, λ h, h.symm ▸ radical_top R⟩
id └─────┘ ┴ ┴ ┴ ┴└───┘ ┴ └─────────┘ ┴
src └─────┘ ┴ └───┘ ┴ └─────────┘
typ └─────┘ ┴ ┴ ┴ ┴└───┘ ┴ └─────────┘ ┴
351
352 theorem is_prime.radical (H : is_prime I) : radical I = I :=
id └──────┘ ┴ └─────┘ ┴ ┴ ┴
src └──────┘ └─────┘ ┴
typ └──────┘ ┴ └─────┘ ┴ ┴ ┴
doc └─────┘
353 le_antisymm (λ r ⟨n, hrni⟩, H.mem_of_pow_mem n hrni) le_radical
id └─────────┘ ┴ ┴┴ └──┘ ┴└─────────────┘ └────────┘
src └─────────┘ └─────────────┘ └────────┘
typ └─────────┘ ┴ ┴┴ └──┘ ┴└─────────────┘ └────────┘
354
355 variables (I J)
356 theorem radical_sup : radical (I ⊔ J) = radical (radical I ⊔ radical J) :=
id └─────┘ ┴ ┴ ┴ ┴ └─────┘ └─────┘ ┴ ┴ └─────┘ ┴
src └─────┘ ┴ ┴ └─────┘ └─────┘ ┴ └─────┘
typ └─────┘ ┴ ┴ ┴ ┴ └─────┘ └─────┘ ┴ ┴ └─────┘ ┴
doc └─────┘ └─────┘ └─────┘ └─────┘
357 le_antisymm (radical_mono $ sup_le_sup le_radical le_radical) $
id └─────────┘ └──────────┘ └────────┘ └────────┘ └────────┘
src └─────────┘ └──────────┘ └────────┘ └────────┘ └────────┘
typ └─────────┘ └──────────┘ └────────┘ └────────┘ └────────┘
358 λ r ⟨n, hrnij⟩, let ⟨s, hs, t, ht, hst⟩ := submodule.mem_sup.1 hrnij in
id ┴ ┴┴ └───┘ └─┘ └┘ └┘ └─┘ └───────────────┘┴
src └───────────────┘┴
typ ┴ ┴┴ └───┘ └─┘ └┘ └┘ └─┘ └───────────────┘┴
359 @radical_idem _ _ (I ⊔ J) ▸ ⟨n, hst ▸ ideal.add_mem _
id └──────────┘ ┴ ┴ ┴ ┴ ┴ └───────────┘
src └──────────┘ ┴ ┴ ┴ └───────────┘
typ └──────────┘ ┴ ┴ ┴ ┴ ┴ └───────────┘
360 (radical_mono le_sup_left hs) (radical_mono le_sup_right ht)⟩
id └──────────┘ └─────────┘ └──────────┘ └──────────┘
src └──────────┘ └─────────┘ └──────────┘ └──────────┘
typ └──────────┘ └─────────┘ └──────────┘ └──────────┘
361
362 theorem radical_inf : radical (I ⊓ J) = radical I ⊓ radical J :=
id └─────┘ ┴ ┴ ┴ ┴ └─────┘ ┴ ┴ └─────┘ ┴
src └─────┘ ┴ ┴ └─────┘ ┴ └─────┘
typ └─────┘ ┴ ┴ ┴ ┴ └─────┘ ┴ ┴ └─────┘ ┴
doc └─────┘ └─────┘ └─────┘
363 le_antisymm (le_inf (radical_mono inf_le_left) (radical_mono inf_le_right))
id └─────────┘ └────┘ └──────────┘ └─────────┘ └──────────┘ └──────────┘
src └─────────┘ └────┘ └──────────┘ └─────────┘ └──────────┘ └──────────┘
typ └─────────┘ └────┘ └──────────┘ └─────────┘ └──────────┘ └──────────┘
364 (λ r ⟨⟨m, hrm⟩, ⟨n, hrn⟩⟩, ⟨m + n, (pow_add r m n).symm ▸ I.mul_mem_right hrm,
id ┴ ┴ ┴ └─┘ ┴ └─┘ ┴ └─────┘ ┴ └──┘ ┴ ┴└────────────┘
src ┴ └─────┘ └──┘ ┴ └────────────┘
typ ┴ ┴ ┴ └─┘ ┴ └─┘ ┴ └─────┘ ┴ └──┘ ┴ ┴└────────────┘
365 (pow_add r m n).symm ▸ J.mul_mem_left hrn⟩)
id └─────┘ ┴ └──┘ ┴ ┴└───────────┘
src └─────┘ └──┘ ┴ └───────────┘
typ └─────┘ ┴ └──┘ ┴ ┴└───────────┘
366
367 theorem radical_mul : radical (I * J) = radical I ⊓ radical J :=
id └─────┘ ┴ ┴ ┴ ┴ └─────┘ ┴ ┴ └─────┘ ┴
src └─────┘ ┴ ┴ └─────┘ ┴ └─────┘
typ └─────┘ ┴ ┴ ┴ ┴ └─────┘ ┴ ┴ └─────┘ ┴
doc └─────┘ └─────┘ └─────┘
368 le_antisymm (radical_inf I J ▸ radical_mono $ @mul_le_inf _ _ I J)
id └─────────┘ └─────────┘ ┴ ┴ ┴ └──────────┘ └────────┘ ┴ ┴
src └─────────┘ └─────────┘ ┴ └──────────┘ └────────┘
typ └─────────┘ └─────────┘ ┴ ┴ ┴ └──────────┘ └────────┘ ┴ ┴
369 (λ r ⟨⟨m, hrm⟩, ⟨n, hrn⟩⟩, ⟨m + n, (pow_add r m n).symm ▸ mul_mem_mul hrm hrn⟩)
id ┴ ┴ ┴ └─┘ ┴ └─┘ ┴ └─────┘ ┴ └──┘ ┴ └─────────┘
src ┴ └─────┘ └──┘ ┴ └─────────┘
typ ┴ ┴ ┴ └─┘ ┴ └─┘ ┴ └─────┘ ┴ └──┘ ┴ └─────────┘
370 variables {I J}
371
372 theorem is_prime.radical_le_iff (hj : is_prime J) :
id └──────┘ ┴
src └──────┘
typ └──────┘ ┴
373 radical I ≤ J ↔ I ≤ J :=
id └─────┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴
src └─────┘ ┴ ┴ ┴
typ └─────┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴
doc └─────┘
374 ⟨le_trans le_radical, λ hij r ⟨n, hrni⟩, hj.mem_of_pow_mem n $ hij hrni⟩
id └──────┘ └────────┘ └─┘ ┴ ┴┴ └──┘ └┘└─────────────┘ └─┘
src └──────┘ └────────┘ └─────────────┘
typ └──────┘ └────────┘ └─┘ ┴ ┴┴ └──┘ └┘└─────────────┘ └─┘
375
376 theorem radical_eq_Inf (I : ideal R) :
id └───┘ ┴
src └───┘
typ └───┘ ┴
377 radical I = Inf { J : ideal R | I ≤ J ∧ is_prime J } :=
id └─────┘ ┴ ┴ └─┘ ┴ └───┘ ┴ ┴ ┴ ┴ ┴ └──────┘ ┴
src └─────┘ ┴ └─┘ ┴ └───┘ ┴ ┴ └──────┘
typ └─────┘ ┴ ┴ └─┘ ┴ └───┘ ┴ ┴ ┴ ┴ ┴ └──────┘ ┴
doc └─────┘ └─┘
378 le_antisymm (le_Inf $ λ J hJ, hJ.2.radical_le_iff.2 hJ.1) $
id └─────────┘ └────┘ ┴ └┘ └┘┴ └────────────┘ ┴ └┘┴
src └─────────┘ └────┘ ┴ └────────────┘ ┴ ┴
typ └─────────┘ └────┘ ┴ └┘ └┘┴ └────────────┘ ┴ └┘┴
379 λ r hr, classical.by_contradiction $ λ hri,
id ┴ └┘ └────────────────────────┘ └─┘
src └────────────────────────┘
typ ┴ └┘ └────────────────────────┘ └─┘
380 let ⟨m, (hrm : r ∉ radical m), him, hm⟩ := zorn.zorn_partial_order₀ {K : ideal R | r ∉ radical K}
id └─┘ ┴ ┴ ┴ ┴ └─────┘ └─┘ └┘ └──────────────────────┘ ┴ └───┘ ┴ ┴ ┴ └─────┘ ┴
src ┴ └─────┘ └──────────────────────┘ ┴ └───┘ ┴ └─────┘
typ └─┘ ┴ ┴ ┴ ┴ └─────┘ └─┘ └┘ └──────────────────────┘ ┴ └───┘ ┴ ┴ ┴ └─────┘ ┴
doc └─────┘ └─────┘
381 (λ c hc hcc y hyc, ⟨Sup c, λ ⟨n, hrnc⟩, let ⟨y, hyc, hrny⟩ :=
id ┴ └┘ └─┘ ┴ └─┘ └─┘ ┴ ┴┴ └──┘ └─┘ └─┘ └──┘
src └─┘
typ ┴ └┘ └─┘ ┴ └─┘ └─┘ ┴ ┴┴ └──┘ └─┘ └─┘ └──┘
doc └─┘
382 submodule.mem_Sup_of_directed hrnc y hyc hcc.directed_on in hc hyc ⟨n, hrny⟩,
id └───────────────────────────┘ ┴ └─┘ └─┘└──────────┘ └┘
src └───────────────────────────┘ └──────────┘
typ └───────────────────────────┘ ┴ └─┘ └─┘└──────────┘ └┘
383 λ z, le_Sup⟩) I hri in
id ┴ └────┘ ┴ └─┘
src └────┘
typ ┴ └────┘ ┴ └─┘
384 have ∀ x ∉ m, r ∈ radical (m ⊔ span {x}) := λ x hxm, classical.by_contradiction $ λ hrmx, hxm $
id ┴ ┴ ┴ └─────┘ ┴ └──┘ ┴┴ ┴ └─┘ └────────────────────────┘ └──┘ └─┘
src ┴ ┴ └─────┘ ┴ └──┘ ┴ └────────────────────────┘
typ ┴ ┴ ┴ └─────┘ ┴ └──┘ ┴┴ ┴ └─┘ └────────────────────────┘ └──┘ └─┘
doc └─────┘
385 hm (m ⊔ span {x}) hrmx le_sup_left ▸ (le_sup_right : _ ≤ m ⊔ span {x}) (subset_span $ set.mem_singleton _),
id ┴ └──┘ ┴┴ └──┘ └─────────┘ ┴ └──────────┘ ┴ ┴ └──┘ ┴┴ └─────────┘ └───────────────┘
src ┴ └──┘ ┴ └─────────┘ ┴ └──────────┘ ┴ ┴ └──┘ ┴ └─────────┘ └───────────────┘
typ ┴ └──┘ ┴┴ └──┘ └─────────┘ ┴ └──────────┘ ┴ ┴ └──┘ ┴┴ └─────────┘ └───────────────┘
386 have is_prime m, from ⟨by rintro rfl; rw radical_top at hrm; exact hrm trivial,
id └──────┘ └─────────┘ └─┘ └─────┘
src └──────┘ └────────┘ └─┘└─────────┘└─────┘ └────┘ ┴└─────┘
typ └──────┘ └────────┘ └─┘└─────────┘└─────┘ └────┘└─┘┴└─────┘
doc └────────┘ └─┘ └─────┘ └────┘ ┴
txt └────────┘ └─┘ └─────┘ └────┘ ┴
par └────────┘ └─┘ └─────┘ └────┘ ┴
pid └──┘ ┴ └─────┘ ┴ ┴
st └──────────────┘└─────────┘└────────────────────────┘
387 λ x y hxym, classical.or_iff_not_imp_left.2 $ λ hxm, classical.by_contradiction $ λ hym,
id ┴ ┴ └──┘ └───────────────────────────┘┴ └─┘ └────────────────────────┘ └─┘
src └───────────────────────────┘┴ └────────────────────────┘
typ ┴ ┴ └──┘ └───────────────────────────┘┴ └─┘ └────────────────────────┘ └─┘
388 let ⟨n, hrn⟩ := this _ hxm, ⟨p, hpm, q, hq, hpqrn⟩ := submodule.mem_sup.1 hrn, ⟨c, hcxq⟩ := mem_span_singleton'.1 hq in
id └─┘ ┴ └─┘ └──┘ └─┘ └┘ └───────────────┘┴ └─────────────────┘┴
src └───────────────┘┴ └─────────────────┘┴
typ └─┘ ┴ └─┘ └──┘ └─┘ └┘ └───────────────┘┴ └─────────────────┘┴
389 let ⟨k, hrk⟩ := this _ hym, ⟨f, hfm, g, hg, hfgrk⟩ := submodule.mem_sup.1 hrk, ⟨d, hdyg⟩ := mem_span_singleton'.1 hg in
id └─┘ ┴ └─┘ └──┘ └─┘ └┘ └───────────────┘┴ └─────────────────┘┴
src └───────────────┘┴ └─────────────────┘┴
typ └─┘ ┴ └─┘ └──┘ └─┘ └┘ └───────────────┘┴ └─────────────────┘┴
390 hrm ⟨n + k, by rw [pow_add, ← hpqrn, ← hcxq, ← hfgrk, ← hdyg, add_mul, mul_add (c*x), mul_assoc c x (d*y), mul_left_comm x, ← mul_assoc];
id ┴ └─────┘ └───┘ └──┘ └───┘ └──┘ └─────┘ └─────┘ ┴┴┴ └───────┘ ┴ ┴ ┴ ┴ └───────────┘ ┴ └───────┘
src ┴ └──┘└─────┘└──┘ └──┘ └──┘ └──┘ └┘└─────┘└┘└─────┘┴ ┴ └─┘└───────┘┴ ┴ ┴ └─┘└───────────┘┴ └──┘└───────┘┴
typ ┴ └──┘└─────┘└──┘└───┘└──┘└──┘└──┘└───┘└──┘└──┘└┘└─────┘└┘└─────┘┴ ┴┴┴└─┘└───────┘┴┴┴┴┴ ┴ ┴└─┘└───────────┘┴┴└──┘└───────┘┴
doc └──┘ └──┘ └──┘ └──┘ └──┘ └┘ └┘ ┴ └─┘ ┴ ┴ ┴ └─┘ ┴ └──┘ ┴
txt └──┘ └──┘ └──┘ └──┘ └──┘ └┘ └┘ ┴ └─┘ ┴ ┴ ┴ └─┘ ┴ └──┘ ┴
par └──┘ └──┘ └──┘ └──┘ └──┘ └┘ └┘ ┴ └─┘ ┴ ┴ ┴ └─┘ ┴ └──┘ ┴
pid └┘ └──┘ └──┘ └──┘ └──┘ └┘ └┘ ┴ └─┘ ┴ ┴ ┴ └─┘ ┴ └──┘ ┴
st └──────────┘└───────┘└──────┘└───────┘└──────┘└───────┘└─────────────┘└───────────────────┘└───────────────┘└───────────┘┴└─
391 refine m.add_mem (m.mul_mem_right hpm) (m.add_mem (m.mul_mem_left hfm) (m.mul_mem_left hxym))⟩⟩,
id └─────────────┘ └─┘ └───────┘ └─┘ └────────────┘ └──┘
src └─────┘ ┴ └─────────────┘┴ └┘ └───────┘┴ ┴ └┘ └────────────┘┴ └┘
typ └─────┘ ┴ └─────────────┘┴└─┘└┘ └───────┘┴ ┴└─┘└┘ └────────────┘┴└──┘└┘
doc └─────┘ ┴ ┴ └┘ ┴ ┴ └┘ ┴ └┘
txt └─────┘ ┴ ┴ └┘ ┴ ┴ └┘ ┴ └┘
par └─────┘ ┴ ┴ └┘ ┴ ┴ └┘ ┴ └┘
pid ┴ ┴ ┴ └┘ ┴ ┴ └┘ ┴ └┘
st ────────────────────────────────────────────────────────────────────────────────────────────────┘
392 hrm $ this.radical.symm ▸ (Inf_le ⟨him, this⟩ : Inf {J : ideal R | I ≤ J ∧ is_prime J} ≤ m) hr
id └──┘└──────┘└───┘ ┴ └────┘ └──┘ └─┘ ┴ └───┘ ┴ ┴ ┴ ┴ ┴ └──────┘ ┴ ┴ └┘
src └──────┘└───┘ ┴ └────┘ └─┘ ┴ └───┘ ┴ ┴ └──────┘ ┴
typ └──┘└──────┘└───┘ ┴ └────┘ └──┘ └─┘ ┴ └───┘ ┴ ┴ ┴ ┴ ┴ └──────┘ ┴ ┴ └┘
doc └─┘
393
394 instance : comm_semiring (ideal R) := submodule.comm_semiring
id └───────────┘ └───┘ ┴ └─────────────────────┘
src └───────────┘ └───┘ └─────────────────────┘
typ └───────────┘ └───┘ ┴ └─────────────────────┘
395
396 @[simp] lemma add_eq_sup : I + J = I ⊔ J := rfl
id ┴ ┴ ┴ ┴ ┴ ┴ ┴ └─┘
src ┴ ┴ ┴ └─┘
typ ┴ ┴ ┴ ┴ ┴ ┴ ┴ └─┘
doc └──┘
397 @[simp] lemma zero_eq_bot : (0 : ideal R) = ⊥ := rfl
id └───┘ ┴ ┴ ┴ └─┘
src └───┘ ┴ ┴ └─┘
typ └───┘ ┴ ┴ ┴ └─┘
doc └──┘
398 @[simp] lemma one_eq_top : (1 : ideal R) = ⊤ :=
id └───┘ ┴ ┴ ┴
src └───┘ ┴ ┴
typ └───┘ ┴ ┴ ┴
doc └──┘
399 by erw [submodule.one_eq_map_top, submodule.map_id]
id └──────────────────────┘ └──────────────┘
src └───┘└──────────────────────┘└┘└──────────────┘└─
typ └───┘└──────────────────────┘└┘└──────────────┘└─
doc └───┘ └┘ └─
txt └───┘ └┘ └─
par └───┘ └┘ └─
pid └┘ └┘ ┴└
st └────────────────────────────┘└────────────────┘┴└
400
src ┘
typ ┘
doc ┘
txt ┘
par ┘
pid ┘
st ┘
401 variables (I)
402 theorem radical_pow (n : ℕ) (H : n > 0) : radical (I^n) = radical I :=
id ┴ ┴ ┴ └─────┘ ┴┴┴ ┴ └─────┘ ┴
src ┴ ┴ └─────┘ ┴ ┴ └─────┘
typ ┴ ┴ ┴ └─────┘ ┴┴┴ ┴ └─────┘ ┴
doc └─────┘ └─────┘
403 nat.rec_on n (not.elim dec_trivial) (λ n ih H,
id └────────┘ ┴ └──────┘ └─────────┘ ┴ └┘ ┴
src └────────┘ └──────┘ └─────────┘
typ └────────┘ ┴ └──────┘ └─────────┘ ┴ └┘ ┴
doc └─────────┘
404 or.cases_on (lt_or_eq_of_le $ nat.le_of_lt_succ H)
id └─────────┘ └────────────┘ └───────────────┘ ┴
src └─────────┘ └────────────┘ └───────────────┘
typ └─────────┘ └────────────┘ └───────────────┘ ┴
405 (λ H, calc radical (I^(n+1))
id ┴ └─────┘ ┴┴ ┴┴
src └─────┘ ┴ ┴
typ ┴ └─────┘ ┴┴ ┴┴
doc └─────┘
406 = radical I ⊓ radical (I^n) : radical_mul _ _
id └─────┘ ┴ ┴ └─────┘ ┴┴┴ └─────────┘
src └─────┘ ┴ └─────┘ ┴ └─────────┘
typ └─────┘ ┴ ┴ └─────┘ ┴┴┴ └─────────┘
doc └─────┘ └─────┘
407 ... = radical I ⊓ radical I : by rw ih H
id └─────┘ ┴ ┴ └─────┘ ┴ └┘ ┴
src └─────┘ ┴ └─────┘ └─┘ ┴ └
typ └─────┘ ┴ ┴ └─────┘ ┴ └─┘└┘┴┴└
doc └─────┘ └─────┘ └─┘ ┴ └
txt └─┘ ┴ └
par └─┘ ┴ └
pid ┴ ┴ └
st └────────
408 ... = radical I : inf_idem)
id └─────┘ ┴ └──────┘
src ──────┘ └─────┘ └──────┘
typ ──────┘ └─────┘ ┴ └──────┘
doc ──────┘ └─────┘
txt ──────┘
par ──────┘
pid ──────┘
st ──────┘
409 (λ H, H ▸ (pow_one I).symm ▸ rfl)) H
id ┴ ┴ ┴ └─────┘ ┴ └──┘ ┴ └─┘ ┴
src ┴ └─────┘ └──┘ ┴ └─┘
typ ┴ ┴ ┴ └─────┘ ┴ └──┘ ┴ └─┘ ┴
410
411 end mul_and_radical
412
413 section map_and_comap
414 variables {R : Type u} {S : Type v} [comm_ring R] [comm_ring S]
id └───────┘ └───────┘
src └───────┘ └───────┘
typ └───────┘ └───────┘
415 variables (f : R → S) [is_ring_hom f]
id └─────────┘
src └─────────┘
typ └─────────┘
doc └─────────┘
416 variables {I J : ideal R} {K L : ideal S}
id └───┘ └───┘
src └───┘ └───┘
typ └───┘ └───┘
417
418 def map (I : ideal R) : ideal S :=
id └───┘ ┴ └───┘ ┴
src └───┘ └───┘
typ └───┘ ┴ └───┘ ┴
419 span (f '' I)
id └──┘ ┴ └┘ ┴
src └──┘ └┘
typ └──┘ ┴ └┘ ┴
420
421 /-- `I.comap f` is the preimage of `I` under `f`. -/
422 def comap (I : ideal S) : ideal R :=
id └───┘ ┴ └───┘ ┴
src └───┘ └───┘
typ └───┘ ┴ └───┘ ┴
423 { carrier := f ⁻¹' I,
id ┴ └─┘ ┴
src └─┘
typ ┴ └─┘ ┴
doc └─┘
424 zero := show f 0 ∈ I, by rw is_ring_hom.map_zero f; exact I.zero_mem,
id ┴ ┴ ┴ └──────────────────┘ ┴ └────────┘
src ┴ └─┘└──────────────────┘┴ └────┘└────────┘
typ ┴ ┴ ┴ └─┘└──────────────────┘┴┴ └────┘└────────┘
doc └─┘└──────────────────┘┴ └────┘
txt └─┘ ┴ └────┘
par └─┘ ┴ └────┘
pid ┴ ┴ ┴
st └──────────────────────────────────────────┘
425 add := λ x y hx hy, show f (x + y) ∈ I, by rw is_ring_hom.map_add f; exact I.add_mem hx hy,
id ┴ ┴ └┘ └┘ ┴ ┴ ┴ ┴ ┴ ┴ └─────────────────┘ ┴ └───────┘ └┘ └┘
src ┴ ┴ └─┘└─────────────────┘┴ └────┘└───────┘┴ ┴
typ ┴ ┴ └┘ └┘ ┴ ┴ ┴ ┴ ┴ ┴ └─┘└─────────────────┘┴┴ └────┘└───────┘┴└┘┴└┘
doc └─┘ ┴ └────┘ ┴ ┴
txt └─┘ ┴ └────┘ ┴ ┴
par └─┘ ┴ └────┘ ┴ ┴
pid ┴ ┴ ┴ ┴ ┴
st └──────────────────────────────────────────────┘
426 smul := λ c x hx, show f (c * x) ∈ I, by rw is_ring_hom.map_mul f; exact I.mul_mem_left hx }
id ┴ ┴ └┘ ┴ ┴ ┴ ┴ ┴ ┴ └─────────────────┘ ┴ └────────────┘ └┘
src ┴ ┴ └─┘└─────────────────┘┴ └────┘└────────────┘┴ ┴
typ ┴ ┴ └┘ ┴ ┴ ┴ ┴ ┴ ┴ └─┘└─────────────────┘┴┴ └────┘└────────────┘┴└┘┴
doc └─┘ ┴ └────┘ ┴ ┴
txt └─┘ ┴ └────┘ ┴ ┴
par └─┘ ┴ └────┘ ┴ ┴
pid ┴ ┴ ┴ ┴ ┴
st └─────────────────────────────────────────────────┘
427
428 variables {f}
429 theorem map_mono (h : I ≤ J) : map f I ≤ map f J :=
id ┴ ┴ ┴ └─┘ ┴ ┴ ┴ └─┘ ┴ ┴
src ┴ └─┘ ┴ └─┘
typ ┴ ┴ ┴ └─┘ ┴ ┴ ┴ └─┘ ┴ ┴
430 span_mono $ set.image_subset _ h
id └───────┘ └──────────────┘ ┴
src └───────┘ └──────────────┘
typ └───────┘ └──────────────┘ ┴
431
432 theorem mem_map_of_mem {x} (h : x ∈ I) : f x ∈ map f I :=
id ┴ ┴ ┴ ┴ ┴ ┴ └─┘ ┴ ┴
src ┴ ┴ └─┘
typ ┴ ┴ ┴ ┴ ┴ ┴ └─┘ ┴ ┴
433 subset_span ⟨x, h, rfl⟩
id └─────────┘ ┴ ┴ └─┘
src └─────────┘ └─┘
typ └─────────┘ ┴ ┴ └─┘
434
435 theorem map_le_iff_le_comap :
436 map f I ≤ K ↔ I ≤ comap f K :=
id └─┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ └───┘ ┴ ┴
src └─┘ ┴ ┴ ┴ └───┘
typ └─┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ └───┘ ┴ ┴
doc └───┘
437 span_le.trans set.image_subset_iff
id └─────┘└────┘ └──────────────────┘
src └─────┘└────┘ └──────────────────┘
typ └─────┘└────┘ └──────────────────┘
doc └──────────────────┘
438
439 @[simp] theorem mem_comap {x} : x ∈ comap f K ↔ f x ∈ K := iff.rfl
id ┴ ┴ └───┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ └─────┘
src ┴ └───┘ ┴ ┴ └─────┘
typ ┴ ┴ └───┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ └─────┘
doc └──┘ └───┘
440
441 theorem comap_mono (h : K ≤ L) : comap f K ≤ comap f L :=
id ┴ ┴ ┴ └───┘ ┴ ┴ ┴ └───┘ ┴ ┴
src ┴ └───┘ ┴ └───┘
typ ┴ ┴ ┴ └───┘ ┴ ┴ ┴ └───┘ ┴ ┴
doc └───┘ └───┘
442 set.preimage_mono h
id └───────────────┘ ┴
src └───────────────┘
typ └───────────────┘ ┴
443 variables (f)
444
445 theorem comap_ne_top (hK : K ≠ ⊤) : comap f K ≠ ⊤ :=
id ┴ ┴ ┴ └───┘ ┴ ┴ ┴ ┴
src ┴ ┴ └───┘ ┴ ┴
typ ┴ ┴ ┴ └───┘ ┴ ┴ ┴ ┴
doc └───┘
446 (ne_top_iff_one _).2 $ by rw [mem_comap, is_ring_hom.map_one f];
id └────────────┘ ┴ └───────┘ └─────────────────┘ ┴
src └────────────┘ ┴ └──┘└───────┘└┘└─────────────────┘┴ ┴
typ └────────────┘ ┴ └──┘└───────┘└┘└─────────────────┘┴┴┴
doc └──┘ └┘ ┴ ┴
txt └──┘ └┘ ┴ ┴
par └──┘ └┘ ┴ ┴
pid └┘ └┘ ┴ ┴
st └────────────┘└─────────────────────┘┴└─
447 exact (ne_top_iff_one _).1 hK
id └────────────┘ └┘
src └────┘ └────────────┘└────┘ └
typ └────┘ └────────────┘└────┘└┘└
doc └────┘ └────┘ └
txt └────┘ └────┘ └
par └────┘ └────┘ └
pid ┴ └────┘ └
st ────────────────────────────────
448
src ┘
typ ┘
doc ┘
txt ┘
par ┘
pid ┘
st ┘
449 instance is_prime.comap [hK : K.is_prime] : (comap f K).is_prime :=
id ┴└───────┘ └───┘ ┴ ┴ └──────┘
src └───────┘ └───┘ └──────┘
typ ┴└───────┘ └───┘ ┴ ┴ └──────┘
doc └───┘
450 ⟨comap_ne_top _ hK.1, λ x y,
id └──────────┘ └┘┴ ┴ ┴
src └──────────┘ ┴
typ └──────────┘ └┘┴ ┴ ┴
451 by simp only [mem_comap, is_ring_hom.map_mul f]; apply hK.2⟩
id └───────┘ └─────────────────┘ ┴ └┘
src └─────────┘└───────┘└┘└─────────────────┘┴ ┴ └────┘ └┘
typ └─────────┘└───────┘└┘└─────────────────┘┴┴┴ └────┘└┘└┘
doc └─────────┘ └┘ ┴ ┴ └────┘ └┘
txt └─────────┘ └┘ ┴ ┴ └────┘ └┘
par └─────────┘ └┘ ┴ ┴ └────┘ └┘
pid ┴└──┘└┘ └┘ ┴ ┴ ┴ └┘
st └───────────────────────────────────────────────────────┘
452
453 variables (I J K L)
454 theorem map_bot : map f ⊥ = ⊥ :=
id └─┘ ┴ ┴ ┴ ┴
src └─┘ ┴ ┴ ┴
typ └─┘ ┴ ┴ ┴ ┴
455 le_antisymm (map_le_iff_le_comap.2 bot_le) bot_le
id └─────────┘ └─────────────────┘┴ └────┘ └────┘
src └─────────┘ └─────────────────┘┴ └────┘ └────┘
typ └─────────┘ └─────────────────┘┴ └────┘ └────┘
456
457 theorem map_top : map f ⊤ = ⊤ :=
id └─┘ ┴ ┴ ┴ ┴
src └─┘ ┴ ┴ ┴
typ └─┘ ┴ ┴ ┴ ┴
458 (eq_top_iff_one _).2 $ subset_span ⟨1, trivial, is_ring_hom.map_one f⟩
id └────────────┘ ┴ └─────────┘ └─────┘ └─────────────────┘ ┴
src └────────────┘ ┴ └─────────┘ └─────┘ └─────────────────┘
typ └────────────┘ ┴ └─────────┘ └─────┘ └─────────────────┘ ┴
459
460 theorem comap_top : comap f ⊤ = ⊤ :=
id └───┘ ┴ ┴ ┴ ┴
src └───┘ ┴ ┴ ┴
typ └───┘ ┴ ┴ ┴ ┴
doc └───┘
461 (eq_top_iff_one _).2 trivial
id └────────────┘ ┴ └─────┘
src └────────────┘ ┴ └─────┘
typ └────────────┘ ┴ └─────┘
462
463 theorem map_sup : map f (I ⊔ J) = map f I ⊔ map f J :=
id └─┘ ┴ ┴ ┴ ┴ ┴ └─┘ ┴ ┴ ┴ └─┘ ┴ ┴
src └─┘ ┴ ┴ └─┘ ┴ └─┘
typ └─┘ ┴ ┴ ┴ ┴ ┴ └─┘ ┴ ┴ ┴ └─┘ ┴ ┴
464 le_antisymm (map_le_iff_le_comap.2 $ sup_le
id └─────────┘ └─────────────────┘┴ └────┘
src └─────────┘ └─────────────────┘┴ └────┘
typ └─────────┘ └─────────────────┘┴ └────┘
465 (map_le_iff_le_comap.1 le_sup_left)
id └─────────────────┘┴ └─────────┘
src └─────────────────┘┴ └─────────┘
typ └─────────────────┘┴ └─────────┘
466 (map_le_iff_le_comap.1 le_sup_right))
id └─────────────────┘┴ └──────────┘
src └─────────────────┘┴ └──────────┘
typ └─────────────────┘┴ └──────────┘
467 (sup_le (map_mono le_sup_left) (map_mono le_sup_right))
id └────┘ └──────┘ └─────────┘ └──────┘ └──────────┘
src └────┘ └──────┘ └─────────┘ └──────┘ └──────────┘
typ └────┘ └──────┘ └─────────┘ └──────┘ └──────────┘
468
469 theorem map_mul : map f (I * J) = map f I * map f J :=
id └─┘ ┴ ┴ ┴ ┴ ┴ └─┘ ┴ ┴ ┴ └─┘ ┴ ┴
src └─┘ ┴ ┴ └─┘ ┴ └─┘
typ └─┘ ┴ ┴ ┴ ┴ ┴ └─┘ ┴ ┴ ┴ └─┘ ┴ ┴
470 le_antisymm (map_le_iff_le_comap.2 $ mul_le.2 $ λ r hri s hsj,
id └─────────┘ └─────────────────┘┴ └────┘┴ ┴ └─┘ ┴ └─┘
src └─────────┘ └─────────────────┘┴ └────┘┴
typ └─────────┘ └─────────────────┘┴ └────┘┴ ┴ └─┘ ┴ └─┘
471 show f (r * s) ∈ _, by rw is_ring_hom.map_mul f;
id ┴ ┴ ┴ ┴ ┴ └─────────────────┘ ┴
src ┴ ┴ └─┘└─────────────────┘┴
typ ┴ ┴ ┴ ┴ ┴ └─┘└─────────────────┘┴┴
doc └─┘ ┴
txt └─┘ ┴
par └─┘ ┴
pid ┴ ┴
st └──────────────────────────
472 exact mul_mem_mul (mem_map_of_mem hri) (mem_map_of_mem hsj))
id └─────────┘ └─┘ └────────────┘ └─┘
src └────┘└─────────┘┴ ┴ └┘ └────────────┘┴ ┴
typ └────┘└─────────┘┴ ┴└─┘└┘ └────────────┘┴└─┘┴
doc └────┘ ┴ ┴ └┘ ┴ ┴
txt └────┘ ┴ ┴ └┘ ┴ ┴
par └────┘ ┴ ┴ └┘ ┴ ┴
pid ┴ ┴ ┴ └┘ ┴ ┴
st ────────────────────────────────────────────────────────────┘
473 (trans_rel_right _ (span_mul_span _ _) $ span_le.2 $
id └─────────────┘ └───────────┘ └─────┘┴
src └─────────────┘ └───────────┘ └─────┘┴
typ └─────────────┘ └───────────┘ └─────┘┴
474 set.bUnion_subset $ λ i ⟨r, hri, hfri⟩,
id └───────────────┘ ┴ ┴ └──┘
src └───────────────┘
typ └───────────────┘ ┴ ┴ └──┘
475 set.bUnion_subset $ λ j ⟨s, hsj, hfsj⟩,
id └───────────────┘ ┴ ┴ └──┘
src └───────────────┘
typ └───────────────┘ ┴ ┴ └──┘
476 set.singleton_subset_iff.2 $ hfri ▸ hfsj ▸
id └──────────────────────┘┴ ┴ ┴
src └──────────────────────┘┴ ┴ ┴
typ └──────────────────────┘┴ ┴ ┴
477 by rw [← is_ring_hom.map_mul f];
id └─────────────────┘ ┴
src └────┘└─────────────────┘┴ ┴
typ └────┘└─────────────────┘┴┴┴
doc └────┘ ┴ ┴
txt └────┘ ┴ ┴
par └────┘ ┴ ┴
pid └──┘ ┴ ┴
st └──────────────────────────┘┴└─
478 exact mem_map_of_mem (mul_mem_mul hri hsj))
id └────────────┘ └─────────┘ └─┘ └─┘
src └────┘└────────────┘┴ └─────────┘┴ ┴ ┴
typ └────┘└────────────┘┴ └─────────┘┴└─┘┴└─┘┴
doc └────┘ ┴ ┴ ┴ ┴
txt └────┘ ┴ ┴ ┴ ┴
par └────┘ ┴ ┴ ┴ ┴
pid ┴ ┴ ┴ ┴ ┴
st ───────────────────────────────────────────┘
479
480 theorem comap_inf : comap f (K ⊓ L) = comap f K ⊓ comap f L := rfl
id └───┘ ┴ ┴ ┴ ┴ ┴ └───┘ ┴ ┴ ┴ └───┘ ┴ ┴ └─┘
src └───┘ ┴ ┴ └───┘ ┴ └───┘ └─┘
typ └───┘ ┴ ┴ ┴ ┴ ┴ └───┘ ┴ ┴ ┴ └───┘ ┴ ┴ └─┘
doc └───┘ └───┘ └───┘
481
482 theorem comap_radical : comap f (radical K) = radical (comap f K) :=
id └───┘ ┴ └─────┘ ┴ ┴ └─────┘ └───┘ ┴ ┴
src └───┘ └─────┘ ┴ └─────┘ └───┘
typ └───┘ ┴ └─────┘ ┴ ┴ └─────┘ └───┘ ┴ ┴
doc └───┘ └─────┘ └─────┘ └───┘
483 le_antisymm (λ r ⟨n, hfrnk⟩, ⟨n, show f (r ^ n) ∈ K,
id └─────────┘ ┴ ┴┴ └───┘ ┴ ┴ ┴ ┴ ┴
src └─────────┘ ┴ ┴
typ └─────────┘ ┴ ┴┴ └───┘ ┴ ┴ ┴ ┴ ┴
484 from (is_semiring_hom.map_pow f r n).symm ▸ hfrnk⟩)
id └─────────────────────┘ ┴ ┴ └──┘ ┴
src └─────────────────────┘ └──┘ ┴
typ └─────────────────────┘ ┴ ┴ └──┘ ┴
485 (λ r ⟨n, hfrnk⟩, ⟨n, is_semiring_hom.map_pow f r n ▸ hfrnk⟩)
id ┴ ┴┴ └───┘ └─────────────────────┘ ┴ ┴ ┴
src └─────────────────────┘ ┴
typ ┴ ┴┴ └───┘ └─────────────────────┘ ┴ ┴ ┴
486
487 @[simp] lemma map_quotient_self :
doc └──┘
488 map (quotient.mk I) I = ⊥ :=
id └─┘ └─────────┘ ┴ ┴ ┴ ┴
src └─┘ └─────────┘ ┴ ┴
typ └─┘ └─────────┘ ┴ ┴ ┴ ┴
489 lattice.eq_bot_iff.2 $ ideal.map_le_iff_le_comap.2 $ λ x hx,
id └────────────────┘┴ └───────────────────────┘┴ ┴ └┘
src └────────────────┘┴ └───────────────────────┘┴
typ └────────────────┘┴ └───────────────────────┘┴ ┴ └┘
490 (submodule.mem_bot I.quotient).2 $ ideal.quotient.eq_zero_iff_mem.2 hx
id └───────────────┘ ┴└───────┘ ┴ └────────────────────────────┘┴ └┘
src └───────────────┘ └───────┘ ┴ └────────────────────────────┘┴
typ └───────────────┘ ┴└───────┘ ┴ └────────────────────────────┘┴ └┘
491
492 variables {I J K L}
493
494 theorem map_inf_le : map f (I ⊓ J) ≤ map f I ⊓ map f J :=
id └─┘ ┴ ┴ ┴ ┴ ┴ └─┘ ┴ ┴ ┴ └─┘ ┴ ┴
src └─┘ ┴ ┴ └─┘ ┴ └─┘
typ └─┘ ┴ ┴ ┴ ┴ ┴ └─┘ ┴ ┴ ┴ └─┘ ┴ ┴
495 map_le_iff_le_comap.2 $ (comap_inf f (map f I) (map f J)).symm ▸
id └─────────────────┘┴ └───────┘ ┴ └─┘ ┴ ┴ └─┘ ┴ ┴ └──┘ ┴
src └─────────────────┘┴ └───────┘ └─┘ └─┘ └──┘ ┴
typ └─────────────────┘┴ └───────┘ ┴ └─┘ ┴ ┴ └─┘ ┴ ┴ └──┘ ┴
496 inf_le_inf (map_le_iff_le_comap.1 $ le_refl _) (map_le_iff_le_comap.1 $ le_refl _)
id └────────┘ └─────────────────┘┴ └─────┘ └─────────────────┘┴ └─────┘
src └────────┘ └─────────────────┘┴ └─────┘ └─────────────────┘┴ └─────┘
typ └────────┘ └─────────────────┘┴ └─────┘ └─────────────────┘┴ └─────┘
497
498 theorem map_radical_le : map f (radical I) ≤ radical (map f I) :=
id └─┘ ┴ └─────┘ ┴ ┴ └─────┘ └─┘ ┴ ┴
src └─┘ └─────┘ ┴ └─────┘ └─┘
typ └─┘ ┴ └─────┘ ┴ ┴ └─────┘ └─┘ ┴ ┴
doc └─────┘ └─────┘
499 map_le_iff_le_comap.2 $ λ r ⟨n, hrni⟩, ⟨n, is_semiring_hom.map_pow f r n ▸ mem_map_of_mem hrni⟩
id └─────────────────┘┴ ┴ ┴┴ └──┘ └─────────────────────┘ ┴ ┴ ┴ └────────────┘
src └─────────────────┘┴ └─────────────────────┘ ┴ └────────────┘
typ └─────────────────┘┴ ┴ ┴┴ └──┘ └─────────────────────┘ ┴ ┴ ┴ └────────────┘
500
501 theorem le_comap_sup : comap f K ⊔ comap f L ≤ comap f (K ⊔ L) :=
id └───┘ ┴ ┴ ┴ └───┘ ┴ ┴ ┴ └───┘ ┴ ┴ ┴ ┴
src └───┘ ┴ └───┘ ┴ └───┘ ┴
typ └───┘ ┴ ┴ ┴ └───┘ ┴ ┴ ┴ └───┘ ┴ ┴ ┴ ┴
doc └───┘ └───┘ └───┘
502 map_le_iff_le_comap.1 $ (map_sup f (comap f K) (comap f L)).symm ▸
id └─────────────────┘┴ └─────┘ ┴ └───┘ ┴ ┴ └───┘ ┴ ┴ └──┘ ┴
src └─────────────────┘┴ └─────┘ └───┘ └───┘ └──┘ ┴
typ └─────────────────┘┴ └─────┘ ┴ └───┘ ┴ ┴ └───┘ ┴ ┴ └──┘ ┴
doc └───┘ └───┘
503 sup_le_sup (map_le_iff_le_comap.2 $ le_refl _) (map_le_iff_le_comap.2 $ le_refl _)
id └────────┘ └─────────────────┘┴ └─────┘ └─────────────────┘┴ └─────┘
src └────────┘ └─────────────────┘┴ └─────┘ └─────────────────┘┴ └─────┘
typ └────────┘ └─────────────────┘┴ └─────┘ └─────────────────┘┴ └─────┘
504
505 theorem le_comap_mul : comap f K * comap f L ≤ comap f (K * L) :=
id └───┘ ┴ ┴ ┴ └───┘ ┴ ┴ ┴ └───┘ ┴ ┴ ┴ ┴
src └───┘ ┴ └───┘ ┴ └───┘ ┴
typ └───┘ ┴ ┴ ┴ └───┘ ┴ ┴ ┴ └───┘ ┴ ┴ ┴ ┴
doc └───┘ └───┘ └───┘
506 map_le_iff_le_comap.1 $ (map_mul f (comap f K) (comap f L)).symm ▸
id └─────────────────┘┴ └─────┘ ┴ └───┘ ┴ ┴ └───┘ ┴ ┴ └──┘ ┴
src └─────────────────┘┴ └─────┘ └───┘ └───┘ └──┘ ┴
typ └─────────────────┘┴ └─────┘ ┴ └───┘ ┴ ┴ └───┘ ┴ ┴ └──┘ ┴
doc └───┘ └───┘
507 mul_mono (map_le_iff_le_comap.2 $ le_refl _) (map_le_iff_le_comap.2 $ le_refl _)
id └──────┘ └─────────────────┘┴ └─────┘ └─────────────────┘┴ └─────┘
src └──────┘ └─────────────────┘┴ └─────┘ └─────────────────┘┴ └─────┘
typ └──────┘ └─────────────────┘┴ └─────┘ └─────────────────┘┴ └─────┘
508
509 section surjective
510 variables (hf : function.surjective f)
id └─────────────────┘
src └─────────────────┘
typ └─────────────────┘
511 include hf
512
513 theorem map_comap_of_surjective (I : ideal S) :
id └───┘ ┴
src └───┘
typ └───┘ ┴
514 map f (comap f I) = I :=
id └─┘ ┴ └───┘ ┴ ┴ ┴ ┴
src └─┘ └───┘ ┴
typ └─┘ ┴ └───┘ ┴ ┴ ┴ ┴
doc └───┘
515 le_antisymm (map_le_iff_le_comap.2 (le_refl _))
id └─────────┘ └─────────────────┘┴ └─────┘
src └─────────┘ └─────────────────┘┴ └─────┘
typ └─────────┘ └─────────────────┘┴ └─────┘
516 (λ s hsi, let ⟨r, hfrs⟩ := hf s in
id ┴ └─┘ └─┘ ┴ └──┘ └┘ ┴
typ ┴ └─┘ └─┘ ┴ └──┘ └┘ ┴
517 hfrs ▸ (mem_map_of_mem $ show f r ∈ I, from hfrs.symm ▸ hsi))
id ┴ └────────────┘ ┴ ┴ ┴ └───┘ ┴ └─┘
src ┴ └────────────┘ ┴ └───┘ ┴
typ ┴ └────────────┘ ┴ ┴ ┴ └───┘ ┴ └─┘
518
519 theorem mem_image_of_mem_map_of_surjective {I : ideal R} {y}
id └───┘ ┴
src └───┘
typ └───┘ ┴
520 (H : y ∈ map f I) : y ∈ f '' I :=
id ┴ ┴ └─┘ ┴ ┴ ┴ ┴ ┴ └┘ ┴
src ┴ └─┘ ┴ └┘
typ ┴ ┴ └─┘ ┴ ┴ ┴ ┴ ┴ └┘ ┴
521 submodule.span_induction H (λ _, id) ⟨0, I.zero_mem, is_ring_hom.map_zero f⟩
id └──────────────────────┘ ┴ ┴ └┘ ┴└───────┘ └──────────────────┘ ┴
src └──────────────────────┘ └┘ └───────┘ └──────────────────┘
typ └──────────────────────┘ ┴ ┴ └┘ ┴└───────┘ └──────────────────┘ ┴
doc └──────────────────────┘ └──────────────────┘
522 (λ y1 y2 ⟨x1, hx1i, hxy1⟩ ⟨x2, hx2i, hxy2⟩, ⟨x1 + x2, I.add_mem hx1i hx2i, hxy1 ▸ hxy2 ▸ is_ring_hom.map_add f⟩)
id └┘ └┘ ┴└┘ └──┘ └──┘ ┴└┘ └──┘ └──┘ ┴ ┴└──────┘ ┴ ┴ └─────────────────┘ ┴
src ┴ └──────┘ ┴ ┴ └─────────────────┘
typ └┘ └┘ ┴└┘ └──┘ └──┘ ┴└┘ └──┘ └──┘ ┴ ┴└──────┘ ┴ ┴ └─────────────────┘ ┴
523 (λ c y ⟨x, hxi, hxy⟩, let ⟨d, hdc⟩ := hf c in ⟨d • x, I.smul_mem _ hxi, hdc ▸ hxy ▸ is_ring_hom.map_mul f⟩)
id ┴ ┴ ┴┴ └─┘ └─┘ └─┘ ┴ └─┘ └┘ ┴ ┴ ┴└───────┘ ┴ ┴ └─────────────────┘ ┴
src ┴ └───────┘ ┴ ┴ └─────────────────┘
typ ┴ ┴ ┴┴ └─┘ └─┘ └─┘ ┴ └─┘ └┘ ┴ ┴ ┴└───────┘ ┴ ┴ └─────────────────┘ ┴
524
525 theorem comap_map_of_surjective (I : ideal R) :
id └───┘ ┴
src └───┘
typ └───┘ ┴
526 comap f (map f I) = I ⊔ comap f ⊥ :=
id └───┘ ┴ └─┘ ┴ ┴ ┴ ┴ ┴ └───┘ ┴ ┴
src └───┘ └─┘ ┴ ┴ └───┘ ┴
typ └───┘ ┴ └─┘ ┴ ┴ ┴ ┴ ┴ └───┘ ┴ ┴
doc └───┘ └───┘
527 le_antisymm (assume r h, let ⟨s, hsi, hfsr⟩ := mem_image_of_mem_map_of_surjective f hf h in
id └─────────┘ ┴ ┴ └─┘ ┴ └─┘ └────────────────────────────────┘ ┴ └┘ ┴
src └─────────┘ └────────────────────────────────┘
typ └─────────┘ ┴ ┴ └─┘ ┴ └─┘ └────────────────────────────────┘ ┴ └┘ ┴
528 submodule.mem_sup.2 ⟨s, hsi, r - s, (submodule.mem_bot S).2 $ by rw [is_ring_hom.map_sub f, hfsr, sub_self],
id └───────────────┘┴ ┴ ┴ └───────────────┘ ┴ ┴ └─────────────────┘ ┴ └──┘ └──────┘
src └───────────────┘┴ ┴ └───────────────┘ ┴ └──┘└─────────────────┘┴ └┘ └┘└──────┘┴
typ └───────────────┘┴ ┴ ┴ └───────────────┘ ┴ ┴ └──┘└─────────────────┘┴┴└┘└──┘└┘└──────┘┴
doc └──┘└─────────────────┘┴ └┘ └┘ ┴
txt └──┘ ┴ └┘ └┘ ┴
par └──┘ ┴ └┘ └┘ ┴
pid └┘ ┴ └┘ └┘ ┴
st └────────────────────────┘└────┘└────────┘┴
529 add_sub_cancel'_right s r⟩)
id └───────────────────┘ ┴
src └───────────────────┘
typ └───────────────────┘ ┴
530 (sup_le (map_le_iff_le_comap.1 (le_refl _)) (comap_mono bot_le))
id └────┘ └─────────────────┘┴ └─────┘ └────────┘ └────┘
src └────┘ └─────────────────┘┴ └─────┘ └────────┘ └────┘
typ └────┘ └─────────────────┘┴ └─────┘ └────────┘ └────┘
531
532 /-- Correspondence theorem -/
533 def order_iso_of_surjective :
534 ((≤) : ideal S → ideal S → Prop) ≃o
id ┴ └───┘ ┴ └───┘ ┴ └┘
src ┴ └───┘ └───┘ └┘
typ ┴ └───┘ ┴ └───┘ ┴ └┘
doc └┘
535 ((≤) : { p : ideal R // comap f ⊥ ≤ p } → { p : ideal R // comap f ⊥ ≤ p } → Prop) :=
id ┴ ┴ └───┘ ┴ └───┘ ┴ ┴ ┴ ┴ ┴ └───┘ ┴ └───┘ ┴ ┴ ┴ ┴
src ┴ ┴ └───┘ └───┘ ┴ ┴ ┴ └───┘ └───┘ ┴ ┴
typ ┴ ┴ └───┘ ┴ └───┘ ┴ ┴ ┴ ┴ ┴ └───┘ ┴ └───┘ ┴ ┴ ┴ ┴
doc └───┘ └───┘
536 { to_fun := λ J, ⟨comap f J, comap_mono bot_le⟩,
id ┴ └───┘ ┴ ┴ └────────┘ └────┘
src └───┘ └────────┘ └────┘
typ ┴ └───┘ ┴ ┴ └────────┘ └────┘
doc └───┘
537 inv_fun := λ I, map f I.1,
id ┴ └─┘ ┴ ┴┴
src └─┘ ┴
typ ┴ └─┘ ┴ ┴┴
538 left_inv := λ J, map_comap_of_surjective f hf J,
id ┴ └─────────────────────┘ ┴ └┘ ┴
src └─────────────────────┘
typ ┴ └─────────────────────┘ ┴ └┘ ┴
539 right_inv := λ I, subtype.eq $ show comap f (map f I.1) = I.1,
id ┴ └────────┘ └───┘ ┴ └─┘ ┴ ┴┴ ┴ ┴┴
src └────────┘ └───┘ └─┘ ┴ ┴ ┴
typ ┴ └────────┘ └───┘ ┴ └─┘ ┴ ┴┴ ┴ ┴┴
doc └───┘
540 from (comap_map_of_surjective f hf I).symm ▸ le_antisymm
id └─────────────────────┘ ┴ └┘ ┴ └──┘ ┴ └─────────┘
src └─────────────────────┘ └──┘ ┴ └─────────┘
typ └─────────────────────┘ ┴ └┘ ┴ └──┘ ┴ └─────────┘
541 (sup_le (le_refl _) I.2) le_sup_left,
id └────┘ └─────┘ ┴┴ └─────────┘
src └────┘ └─────┘ ┴ └─────────┘
typ └────┘ └─────┘ ┴┴ └─────────┘
542 ord := λ I1 I2, ⟨comap_mono, λ H, map_comap_of_surjective f hf I1 ▸
id └┘ └┘ └────────┘ ┴ └─────────────────────┘ ┴ └┘ └┘ ┴
src └────────┘ └─────────────────────┘ ┴
typ └┘ └┘ └────────┘ ┴ └─────────────────────┘ ┴ └┘ └┘ ┴
543 map_comap_of_surjective f hf I2 ▸ map_mono H⟩ }
id └─────────────────────┘ ┴ └┘ └┘ ┴ └──────┘ ┴
src └─────────────────────┘ ┴ └──────┘
typ └─────────────────────┘ ┴ └┘ └┘ ┴ └──────┘ ┴
544
545 def le_order_embedding_of_surjective :
546 ((≤) : ideal S → ideal S → Prop) ≼o ((≤) : ideal R → ideal R → Prop) :=
id ┴ └───┘ ┴ └───┘ ┴ └┘ ┴ └───┘ ┴ └───┘ ┴
src ┴ └───┘ └───┘ └┘ ┴ └───┘ └───┘
typ ┴ └───┘ ┴ └───┘ ┴ └┘ ┴ └───┘ ┴ └───┘ ┴
doc └┘
547 (order_iso_of_surjective f hf).to_order_embedding.trans (subtype.order_embedding _ _)
id └─────────────────────┘ ┴ └┘ └────────────────┘ └───┘ └─────────────────────┘
src └─────────────────────┘ └────────────────┘ └───┘ └─────────────────────┘
typ └─────────────────────┘ ┴ └┘ └────────────────┘ └───┘ └─────────────────────┘
doc └─────────────────────┘ └─────────────────────┘
548
549 def lt_order_embedding_of_surjective :
550 ((<) : ideal S → ideal S → Prop) ≼o ((<) : ideal R → ideal R → Prop) :=
id ┴ └───┘ ┴ └───┘ ┴ └┘ ┴ └───┘ ┴ └───┘ ┴
src ┴ └───┘ └───┘ └┘ ┴ └───┘ └───┘
typ ┴ └───┘ ┴ └───┘ ┴ └┘ ┴ └───┘ ┴ └───┘ ┴
doc └┘
551 (le_order_embedding_of_surjective f hf).lt_embedding_of_le_embedding
id └──────────────────────────────┘ ┴ └┘ └──────────────────────────┘
src └──────────────────────────────┘ └──────────────────────────┘
typ └──────────────────────────────┘ ┴ └┘ └──────────────────────────┘
552
553 end surjective
554
555 end map_and_comap
556
557 end ideal
558
559 namespace is_ring_hom
560
561 variables {R : Type u} {S : Type v} (f : R → S) [comm_ring R]
id └───────┘
src └───────┘
typ └───────┘
562
563 section comm_ring
564 variables [comm_ring S] [is_ring_hom f]
id └───────┘ └─────────┘
src └───────┘ └─────────┘
typ └───────┘ └─────────┘
doc └─────────┘
565
566 def ker : ideal R := ideal.comap f ⊥
id └───┘ ┴ └─────────┘ ┴ ┴
src └───┘ └─────────┘ ┴
typ └───┘ ┴ └─────────┘ ┴ ┴
doc └─────────┘
567
568 /-- An element is in the kernel if and only if it maps to zero.-/
569 lemma mem_ker {r} : r ∈ ker f ↔ f r = 0 :=
id ┴ ┴ └─┘ ┴ ┴ ┴ ┴ ┴
src ┴ └─┘ ┴ ┴
typ ┴ ┴ └─┘ ┴ ┴ ┴ ┴ ┴
570 by rw [ker, ideal.mem_comap, submodule.mem_bot]
id └─┘ └─────────────┘ └───────────────┘
src └──┘└─┘└┘└─────────────┘└┘└───────────────┘└─
typ └──┘└─┘└┘└─────────────┘└┘└───────────────┘└─
doc └──┘ └┘ └┘ └─
txt └──┘ └┘ └┘ └─
par └──┘ └┘ └┘ └─
pid └┘ └┘ └┘ ┴└
st └──────┘└───────────────┘└─────────────────┘┴└
571
src ┘
typ ┘
doc ┘
txt ┘
par ┘
pid ┘
st ┘
572 lemma ker_eq : ((ker f) : set R) = is_add_group_hom.ker f := rfl
id └─┘ ┴ └─┘ ┴ ┴ └──────────────────┘ ┴ └─┘
src └─┘ └─┘ ┴ └──────────────────┘ └─┘
typ └─┘ ┴ └─┘ ┴ ┴ └──────────────────┘ ┴ └─┘
573
574 lemma inj_iff_ker_eq_bot : function.injective f ↔ ker f = ⊥ :=
id └────────────────┘ ┴ ┴ └─┘ ┴ ┴ ┴
src └────────────────┘ ┴ └─┘ ┴ ┴
typ └────────────────┘ ┴ ┴ └─┘ ┴ ┴ ┴
575 by rw [←submodule.ext'_iff, ker_eq]; exact is_add_group_hom.inj_iff_trivial_ker f
id └────────────────┘ └────┘ └──────────────────────────────────┘ ┴
src └───┘└────────────────┘└┘└────┘┴ └────┘└──────────────────────────────────┘┴ └
typ └───┘└────────────────┘└┘└────┘┴ └────┘└──────────────────────────────────┘┴┴└
doc └───┘ └┘ ┴ └────┘ ┴ └
txt └───┘ └┘ ┴ └────┘ ┴ └
par └───┘ └┘ ┴ └────┘ ┴ └
pid └─┘ └┘ ┴ ┴ ┴ └
st └──────────────────────┘└──────┘┴└──────────────────────────────────────────────
576
src ┘
typ ┘
doc ┘
txt ┘
par ┘
pid ┘
st ┘
577 lemma ker_eq_bot_iff_eq_zero : ker f = ⊥ ↔ ∀ x, f x = 0 → x = 0 :=
id └─┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴
src └─┘ ┴ ┴ ┴ ┴ ┴
typ └─┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴
578 by rw [←submodule.ext'_iff, ker_eq]; exact is_add_group_hom.trivial_ker_iff_eq_zero f
id └────────────────┘ └────┘ └──────────────────────────────────────┘ ┴
src └───┘└────────────────┘└┘└────┘┴ └────┘└──────────────────────────────────────┘┴ └
typ └───┘└────────────────┘└┘└────┘┴ └────┘└──────────────────────────────────────┘┴┴└
doc └───┘ └┘ ┴ └────┘ ┴ └
txt └───┘ └┘ ┴ └────┘ ┴ └
par └───┘ └┘ ┴ └────┘ ┴ └
pid └─┘ └┘ ┴ ┴ ┴ └
st └──────────────────────┘└──────┘┴└──────────────────────────────────────────────────
579
src ┘
typ ┘
doc ┘
txt ┘
par ┘
pid ┘
st ┘
580 lemma injective_iff : function.injective f ↔ ∀ x, f x = 0 → x = 0 :=
id └────────────────┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴
src └────────────────┘ ┴ ┴ ┴
typ └────────────────┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴
581 is_add_group_hom.injective_iff f
id └────────────────────────────┘ ┴
src └────────────────────────────┘
typ └────────────────────────────┘ ┴
582
583 end comm_ring
584
585 /-- If the target is not the zero ring, then one is not in the kernel.-/
586 lemma not_one_mem_ker [nonzero_comm_ring S] [is_ring_hom f] : (1:R) ∉ ker f :=
id └───────────────┘ ┴ └─────────┘ ┴ ┴ ┴ └─┘ ┴
src └───────────────┘ └─────────┘ ┴ └─┘
typ └───────────────┘ ┴ └─────────┘ ┴ ┴ ┴ └─┘ ┴
doc └───────────────┘ └─────────┘
587 by { rw [mem_ker, is_ring_hom.map_one f], exact one_ne_zero }
id └─────┘ └─────────────────┘ ┴ └─────────┘
src └──┘└─────┘└┘└─────────────────┘┴ ┴ └────┘└─────────┘┴
typ └──┘└─────┘└┘└─────────────────┘┴┴┴ └────┘└─────────┘┴
doc └──┘└─────┘└┘ ┴ ┴ └────┘ ┴
txt └──┘ └┘ ┴ ┴ └────┘ ┴
par └──┘ └┘ ┴ ┴ └────┘ ┴
pid └┘ └┘ ┴ ┴ ┴ ┴
st └────────────┘└─────────────────────┘└───────────────────┘└┘
588
589 /-- The kernel of a homomorphism to an integral domain is a prime ideal.-/
590 lemma ker_is_prime [integral_domain S] [is_ring_hom f] :
id └─────────────┘ ┴ └─────────┘ ┴
src └─────────────┘ └─────────┘
typ └─────────────┘ ┴ └─────────┘ ┴
doc └─────────┘
591 (ker f).is_prime :=
id └─┘ ┴ └──────┘
src └─┘ └──────┘
typ └─┘ ┴ └──────┘
592 ⟨by { rw [ne.def, ideal.eq_top_iff_one], exact not_one_mem_ker f },
id └────┘ └──────────────────┘ └─────────────┘ ┴
src └──┘└────┘└┘└──────────────────┘┴ └────┘└─────────────┘┴ ┴
typ └──┘└────┘└┘└──────────────────┘┴ └────┘└─────────────┘┴┴┴
doc └──┘ └┘ ┴ └────┘└─────────────┘┴ ┴
txt └──┘ └┘ ┴ └────┘ ┴ ┴
par └──┘ └┘ ┴ └────┘ ┴ ┴
pid └┘ └┘ ┴ ┴ ┴ ┴
st └───────────┘└────────────────────┘└─────────────────────────┘└┘
593 λ x y, by simpa only [mem_ker, is_ring_hom.map_mul f] using eq_zero_or_eq_zero_of_mul_eq_zero⟩
id ┴ ┴ └─────┘ └─────────────────┘ ┴ └───────────────────────────────┘
src └──────────┘└─────┘└┘└─────────────────┘┴ └──────┘└───────────────────────────────┘
typ ┴ ┴ └──────────┘└─────┘└┘└─────────────────┘┴┴└──────┘└───────────────────────────────┘
doc └──────────┘└─────┘└┘ ┴ └──────┘
txt └──────────┘ └┘ ┴ └──────┘
par └──────────┘ └┘ ┴ └──────┘
pid ┴└──┘└┘ └┘ ┴ ┴┴└────┘
st └──────────────────────────────────────────────────────────────────────────────────┘
594
595 end is_ring_hom
596
597 namespace submodule
598
599 variables {R : Type u} {M : Type v}
600 variables [comm_ring R] [add_comm_group M] [module R M]
id └───────┘ └────────────┘ └────┘
src └───────┘ └────────────┘ └────┘
typ └───────┘ └────────────┘ └────┘
doc └────┘
601
602 -- It is even a semialgebra. But those aren't in mathlib yet.
603
604 instance : semimodule (ideal R) (submodule R M) :=
id └────────┘ └───┘ ┴ └───────┘ ┴ ┴
src └────────┘ └───┘ └───────┘
typ └────────┘ └───┘ ┴ └───────┘ ┴ ┴
doc └────────┘ └───────┘
605 { smul_add := smul_sup,
id └──────┘
src └──────┘
typ └──────┘
606 add_smul := sup_smul,
id └──────┘
src └──────┘
typ └──────┘
607 mul_smul := smul_assoc,
id └────────┘
src └────────┘
typ └────────┘
608 one_smul := by simp,
src └──┘
typ └──┘
doc └──┘
txt └──┘
par └──┘
st └───┘
609 zero_smul := bot_smul,
id └──────┘
src └──────┘
typ └──────┘
610 smul_zero := smul_bot }
id └──────┘
src └──────┘
typ └──────┘
611
612 end submodule